# HG changeset patch
# User wenzelm
# Date 1392926355 -3600
# Node ID 460f4801b5cbd49bae6a6ca049ae7159f73d6367
# Parent  0f9d03649a9c1efcb88f59d3dcd3d78c9b5a97b6
clarified printing of undeclared hyps;

diff -r 0f9d03649a9c -r 460f4801b5cb src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Feb 20 20:19:41 2014 +0100
+++ b/src/Pure/display.ML	Thu Feb 20 20:59:15 2014 +0100
@@ -55,22 +55,21 @@
 
     val th = Thm.strip_shyps raw_th;
     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
-    val xshyps = Thm.extra_shyps th;
+    val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th;
+    val extra_shyps = Thm.extra_shyps th;
     val tags = Thm.get_tags th;
 
     val q = if quote then Pretty.quote else I;
     val prt_term = q o Syntax.pretty_term ctxt;
 
-    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
-    val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
 
-    val hlen = length xshyps + length hyps' + length tpairs;
+    val hlen = length extra_shyps + length hyps' + length tpairs;
     val hsymbs =
       if hlen = 0 then []
       else if show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
-           map (Syntax.pretty_sort ctxt) xshyps)]
+           map (Syntax.pretty_sort ctxt) extra_shyps)]
       else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
     val tsymbs =
       if null tags orelse not show_tags then []
diff -r 0f9d03649a9c -r 460f4801b5cb src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Feb 20 20:19:41 2014 +0100
+++ b/src/Pure/more_thm.ML	Thu Feb 20 20:59:15 2014 +0100
@@ -55,6 +55,7 @@
   val assume_hyps: cterm -> Proof.context -> thm * Proof.context
   val unchecked_hyps: Proof.context -> Proof.context
   val restore_hyps: Proof.context -> Proof.context -> Proof.context
+  val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
@@ -281,26 +282,26 @@
 val unchecked_hyps = (Hyps.map o apsnd) (K false);
 fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
 
+fun undeclared_hyps context th =
+  Thm.hyps_of th
+  |> filter_out
+    (case context of
+      Context.Theory _ => K false
+    | Context.Proof ctxt =>
+        (case Hyps.get ctxt of
+          (_, false) => K true
+        | (hyps, _) => Termtab.defined hyps));
+
 fun check_hyps context th =
-  let
-    val declared_hyps =
-      (case context of
-        Context.Theory _ => K false
-      | Context.Proof ctxt =>
-          (case Hyps.get ctxt of
-            (_, false) => K true
-          | (hyps, _) => Termtab.defined hyps));
-    val undeclared = filter_out declared_hyps (Thm.hyps_of th);
-  in
-    if null undeclared then th
-    else
+  (case undeclared_hyps context th of
+    [] => th
+  | undeclared =>
       let
         val ctxt = Context.cases Syntax.init_pretty_global I context;
       in
         error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
           (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
-      end
-  end;
+      end);