diff -r ac6af184bfb0 -r 6fb553dc039b src/Pure/Isar/proof_context.ML
--- 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