# HG changeset patch
# User wenzelm
# Date 938605848 -7200
# Node ID 102a4b6b83a60544ceefa4a5f3126c8cafcf21af
# Parent  4c1d2eb68db82546b76e5b3753bb7a7dd2d8c0ac
strip_shyps_warning;

diff -r 4c1d2eb68db8 -r 102a4b6b83a6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Sep 29 13:50:26 1999 +0200
+++ b/src/Pure/drule.ML	Wed Sep 29 13:50:48 1999 +0200
@@ -20,6 +20,7 @@
                   -> string list -> (string*string)list
                   -> (indexname*ctyp)list * (cterm*cterm)list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
+  val strip_shyps_warning : thm -> thm
   val forall_intr_list	: cterm list -> thm -> thm
   val forall_intr_frees	: thm -> thm
   val forall_intr_vars	: thm -> thm
@@ -197,8 +198,21 @@
         fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
     in (typ,sort) end;
 
+
 (** Standardization of rules **)
 
+(*Strip extraneous shyps as far as possible*)
+fun strip_shyps_warning thm =
+  let
+    val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm);
+    val thm' = Thm.strip_shyps thm;
+    val xshyps = Thm.extra_shyps thm';
+  in
+    if null xshyps then ()
+    else warning ("Pending sort hypotheses: " ^ commas (map str_of_sort xshyps));
+    thm'
+  end;
+
 (*Generalization over a list of variables, IGNORING bad ones*)
 fun forall_intr_list [] th = th
   | forall_intr_list (y::ys) th =
@@ -264,7 +278,7 @@
   in
     th |> implies_intr_hyps
        |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
-       |> Thm.strip_shyps |> Thm.implies_intr_shyps
+       |> strip_shyps_warning
        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   end;