# HG changeset patch
# User wenzelm
# Date 1224189870 -7200
# Node ID a60164e8fff0418c59be090f1c43e4f864338b2c
# Parent  9846d772b30649488046fc570384f472106f6a05
added check_shyps, which reject pending sort hypotheses;

diff -r 9846d772b306 -r a60164e8fff0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Oct 16 22:44:29 2008 +0200
+++ b/src/Pure/more_thm.ML	Thu Oct 16 22:44:30 2008 +0200
@@ -27,6 +27,7 @@
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val equiv_thm: thm * thm -> bool
+  val check_shyps: sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
@@ -160,6 +161,20 @@
   Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
 
 
+(* sort hypotheses *)
+
+fun check_shyps sorts raw_th =
+  let
+    val th = Thm.strip_shyps raw_th;
+    val prt_sort = Syntax.pretty_sort_global (Thm.theory_of_thm th);
+    val pending = Sorts.subtract sorts (Thm.extra_shyps th);
+  in
+    if null pending then th
+    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
+      Pretty.brk 1 :: Pretty.commas (map prt_sort pending))))
+  end;
+
+
 (* misc operations *)
 
 fun is_dummy thm =