--- a/src/Pure/Isar/proof_context.ML Wed Jun 10 11:14:46 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 10 11:52:54 2015 +0200
@@ -1385,12 +1385,12 @@
else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
Pretty.commas (map prt_fix fixes))];
- (*prems*)
- val prt_prems =
+ (*assumptions*)
+ val prt_assms =
(case Assumption.all_prems_of ctxt of
[] => []
- | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
- in prt_structs @ prt_fixes @ prt_prems end;
+ | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
+ in prt_structs @ prt_fixes @ prt_assms end;
(* main context *)