# HG changeset patch
# User wenzelm
# Date 1433929974 -7200
# Node ID 0824fd1e9c406c9539c2fb2e867f1b51618fdb88
# Parent  285c7ff27728668255a2b1e5693b15ed55b4ddb4
tuned message;

diff -r 285c7ff27728 -r 0824fd1e9c40 src/Pure/Isar/proof_context.ML
--- 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 *)