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/Pure/Isar/proof_context.ML
changeset 21583 6fb553dc039b
parent 21569 a0d0ea84521d
child 21593 282c40fb001a 
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 29 04:11:15 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Nov 29 04:11:16 2006 +0100
@@ -317,7 +317,7 @@
     val thy = theory_of ctxt;
     val (pp, asms) =
       if Theory.eq_thy (thy, ProtoPure.thy) then (Sign.pp thy, [])
-      else (pp ctxt, Assumption.assms_of ctxt);
+      else (pp ctxt, map Thm.term_of (Assumption.assms_of ctxt));
   in Display.pretty_thm_aux pp false true asms th end;
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
isabelle