Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/coherent.ML
changeset 32091 30e2ffbba718
parent 32035 8e77b6a250d5
child 32199 82c4c570310a 
--- a/src/Tools/coherent.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/coherent.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -177,7 +177,7 @@
 fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   let
     val _ = message (fn () => space_implode "\n"
-      ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
+      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
     val th' = Drule.implies_elim_list
       (Thm.instantiate
          (map (fn (ixn, (S, T)) =>
isabelle