# 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;