Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed export_standard_morphism;
authorwenzelm
Wed, 29 Nov 2006 04:11:16 +0100
changeset 21583 6fb553dc039b
parent 21582 ac6af184bfb0
child 21584 22c9392de970
removed export_standard_morphism; Assumption.assms_of: cterm;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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