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.
pretty_thm: graceful treatment of ProtoPure.thy;
authorwenzelm
Mon, 18 Sep 2006 19:12:47 +0200
changeset 20575 6b1c69265331
parent 20574 a10885a269cb
child 20576 8b1591393b8d
pretty_thm: graceful treatment of ProtoPure.thy;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 18 19:12:46 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 18 19:12:47 2006 +0200
@@ -296,7 +296,12 @@
   in Display.pretty_thm_aux pp quote false [] th end;
 
 fun pretty_thm ctxt th =
-  Display.pretty_thm_aux (pp ctxt) false true (Assumption.assms_of ctxt) th;
+  let
+    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);
+  in Display.pretty_thm_aux pp false true asms th end;
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
isabelle