# HG changeset patch
# User wenzelm
# Date 938606553 -7200
# Node ID 40d912f78db84e5230e1ae3df2d09aba51a2d05d
# Parent  f058df34827222e5ff35856f0d2c621411c9c64b
removed implies_intr_shyps;
removed force_strip_shyps (at last!);
strip_shyps: proper witness_sorts;
fix_shyps: tuned for all_sorts_nonempty;

diff -r f058df348272 -r 40d912f78db8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Sep 29 13:55:58 1999 +0200
+++ b/src/Pure/thm.ML	Wed Sep 29 14:02:33 1999 +0200
@@ -50,7 +50,6 @@
     | Theorem             of string * tag list
     | Assume              of cterm
     | Implies_intr        of cterm
-    | Implies_intr_shyps
     | Implies_intr_hyps
     | Implies_elim 
     | Forall_intr         of cterm
@@ -101,9 +100,7 @@
   val concl_of          : thm -> term
   val cprop_of          : thm -> cterm
   val extra_shyps       : thm -> sort list
-  val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   val strip_shyps       : thm -> thm
-  val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> xstring -> thm
   val def_name		: string -> string
   val get_def           : theory -> xstring -> thm
@@ -326,7 +323,6 @@
 (*primitive inferences and compound versions of them*)
   | Assume              of cterm
   | Implies_intr        of cterm
-  | Implies_intr_shyps
   | Implies_intr_hyps
   | Implies_elim 
   | Forall_intr         of cterm
@@ -524,81 +520,47 @@
 
 fun add_thms_shyps ([], Ss) = Ss
   | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
-      add_thms_shyps (ths, union_sort(shyps,Ss));
+      add_thms_shyps (ths, union_sort (shyps, Ss));
 
 
 (*get 'dangling' sort constraints of a thm*)
 fun extra_shyps (th as Thm {shyps, ...}) =
-  shyps \\ add_thm_sorts (th, []);
+  Term.rems_sort (shyps, add_thm_sorts (th, []));
 
 
 (* fix_shyps *)
 
+fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref));
+
 (*preserve sort contexts of rule premises and substituted types*)
-fun fix_shyps thms Ts thm =
-  let
-    val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm;
-    val shyps =
-      add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
-  in
-    Thm {sign_ref = sign_ref,
-         der = der,             (*No new derivation, as other rules call this*)
-         maxidx = maxidx,
-         shyps = shyps, hyps = hyps, prop = prop}
-  end;
+fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) =
+  Thm
+   {sign_ref = sign_ref,
+    der = der,             (*no new derivation, as other rules call this*)
+    maxidx = maxidx,
+    shyps =
+      if all_sorts_nonempty sign_ref then []
+      else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
+    hyps = hyps, prop = prop}
 
 
-(* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
-
-val force_strip_shyps = ref true;  (* FIXME tmp (since 1995/08/01) *)
+(* strip_shyps *)
 
-(*remove extra sorts that are known to be syntactically non-empty*)
-fun strip_shyps thm =
-  let
-    val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
-    val sorts = add_thm_sorts (thm, []);
-    val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts;
-    val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
-  in
-    Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
-         shyps =
-         (if eq_set_sort (shyps',sorts) orelse 
-             not (!force_strip_shyps) then shyps'
-          else    (* FIXME tmp (since 1995/08/01) *)
-              (warning ("Removed sort hypotheses: " ^
-                        commas (map Sorts.str_of_sort (shyps' \\ sorts)));
-               warning "Let's hope these sorts are non-empty!";
-           sorts)),
-      hyps = hyps, 
-      prop = prop}
-  end;
-
+(*remove extra sorts that are non-empty by virtue of type signature information*)
+fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
+  | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+      let
+        val sign = Sign.deref sign_ref;
 
-(* implies_intr_shyps *)
+        val present_sorts = add_thm_sorts (thm, []);
+        val extra_shyps = Term.rems_sort (shyps, present_sorts);
+        val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
+      in
+        Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
+             shyps = Term.rems_sort (shyps, map #2 witnessed_shyps),
+             hyps = hyps, prop = prop}
+      end;
 
-(*discharge all extra sort hypotheses*)
-fun implies_intr_shyps thm =
-  (case extra_shyps thm of
-    [] => thm
-  | xshyps =>
-      let
-        val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
-        val shyps' = ins_sort (logicS, shyps \\ xshyps);
-        val used_names = foldr add_term_tfree_names (prop :: hyps, []);
-        val names =
-          tl (variantlist (replicate (length xshyps + 1) "'", used_names));
-        val tfrees = map (TFree o rpair logicS) names;
-
-        fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
-        val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
-      in
-        Thm {sign_ref = sign_ref, 
-             der = infer_derivs (Implies_intr_shyps, [der]), 
-             maxidx = maxidx, 
-             shyps = shyps',
-             hyps = hyps, 
-             prop = Logic.list_implies (sort_hyps, prop)}
-      end);
 
 
 (** Axioms **)