# HG changeset patch
# User wenzelm
# Date 1158599567 -7200
# Node ID 6b1c69265331214b641d3e20af45b4f2742ad8e0
# Parent  a10885a269cb762d29aa71eb2fbbc832c0e37e16
pretty_thm: graceful treatment of ProtoPure.thy;

diff -r a10885a269cb -r 6b1c69265331 src/Pure/Isar/proof_context.ML
--- 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));