# HG changeset patch
# User wenzelm
# Date 1445614218 -7200
# Node ID 358dfae15d834f27b747d6d3337281f0b92be495
# Parent  2c7e2ae6173d9ccd6cc4856578417c037cedb91c
print thm wrt. local shyps (from full proof context);
tuned;

diff -r 2c7e2ae6173d -r 358dfae15d83 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Oct 23 17:17:11 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 23 17:30:18 2015 +0200
@@ -63,6 +63,7 @@
   val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
   val declare_term_sorts: term -> Proof.context -> Proof.context
+  val extra_shyps': Proof.context -> thm -> sort list
   val check_shyps: Proof.context -> thm -> thm
   val weaken_sorts': Proof.context -> cterm -> cterm
   val elim_implies: thm -> thm -> thm
@@ -318,14 +319,17 @@
   map_hyps (fn (checked_hyps, hyps, shyps) =>
     (checked_hyps, hyps, Sorts.insert_term t shyps));
 
+fun extra_shyps' ctxt th =
+  Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
+
 fun check_shyps ctxt raw_th =
   let
     val th = Thm.strip_shyps raw_th;
-    val pending = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
+    val extra_shyps = extra_shyps' ctxt th;
   in
-    if null pending then th
+    if null extra_shyps then th
     else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
-      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
+      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps))))
   end;
 
 val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
@@ -663,7 +667,7 @@
       |> perhaps (try Thm.strip_shyps);
 
     val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
-    val extra_shyps = Thm.extra_shyps th;
+    val extra_shyps = extra_shyps' ctxt th;
     val tags = Thm.get_tags th;
     val tpairs = Thm.tpairs_of th;