diff options
Diffstat (limited to 'isa/depends.ML')
| -rw-r--r-- | isa/depends.ML | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/isa/depends.ML b/isa/depends.ML index a8b45d2c..d55b7552 100644 --- a/isa/depends.ML +++ b/isa/depends.ML @@ -60,12 +60,12 @@ fun thm_deps thms = fun new_thm_deps thms = let - val _ = print "Proof General, the theorem dependencies are: "; + val header = "Proof General, the theorem dependencies are: \""; val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), map (#der o rep_thm) thms)))); - fun printname s = (print s; print " "); - val _ = seq printname (foldl (op@) ([],(map #parents gra))); - in writeln "" end; + val deps = foldl (op@) ([],(map #parents gra)) + val msg = header ^ (space_implode " " deps) ^ "\"" + in writeln msg end; val old_qed = qed; |