# HG changeset patch
# User wenzelm
# Date 807290517 -7200
# Node ID 3b0b8408fc5f5825e56994def6d3ac4164873922
# Parent  b1a04399f530bf4f248b681cf7178803eeafd563
MAJOR changes:
  added shyps component to type thm;
  added rules strip_shyps, implies_intr_shyps;
  fixed rules to handle shyps properly;

diff -r b1a04399f530 -r 3b0b8408fc5f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 01 17:21:05 1995 +0200
+++ b/src/Pure/thm.ML	Tue Aug 01 17:21:57 1995 +0200
@@ -36,8 +36,8 @@
   (*meta theorems*)
   type thm
   exception THM of string * int * thm list
-  val rep_thm		: thm ->
-    {sign: Sign.sg, maxidx: int, hyps: term list, prop: term};
+  val rep_thm		: thm -> {sign: Sign.sg, maxidx: int,
+    shyps: sort list, hyps: term list, prop: term}
   val stamps_of_thm	: thm -> string ref list
   val tpairs_of		: thm -> (term * term) list
   val prems_of		: thm -> term list
@@ -93,6 +93,9 @@
   val merge_thy_list	: bool -> theory list -> theory
 
   (*meta rules*)
+  val force_strip_shyps	: bool ref	(* FIXME tmp *)
+  val strip_shyps	: thm -> thm
+  val implies_intr_shyps: thm -> thm
   val assume		: cterm -> thm
   val implies_intr	: cterm -> thm -> thm
   val implies_elim	: thm -> thm -> thm
@@ -220,10 +223,36 @@
 
 
 
+(* FIXME -> library.ML *)
+
+fun unions [] = []
+  | unions (xs :: xss) = foldr (op union) (xss, xs);
+
+
+(* FIXME -> term.ML *)
+
+(*accumulates the sorts in a type, suppressing duplicates*)
+fun add_typ_sorts (Type (_, Ts), Ss) = foldr add_typ_sorts (Ts, Ss)
+  | add_typ_sorts (TFree (_, S), Ss) = S ins Ss
+  | add_typ_sorts (TVar (_, S), Ss) = S ins Ss;
+
+val add_term_sorts = it_term_types add_typ_sorts;
+
+fun typ_sorts T = add_typ_sorts (T, []);
+fun term_sorts t = add_term_sorts (t, []);
+
+
+(* FIXME move? *)
+
+fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
+
+
+
 (*** Meta theorems ***)
 
 datatype thm = Thm of
-  {sign: Sign.sg, maxidx: int, hyps: term list, prop: term};
+  {sign: Sign.sg, maxidx: int,
+    shyps: sort list, hyps: term list, prop: term};
 
 fun rep_thm (Thm args) = args;
 
@@ -295,8 +324,8 @@
     fun get_ax [] = raise Match
       | get_ax (Theory {sign, new_axioms, parents} :: thys) =
           (case Symtab.lookup (new_axioms, name) of
-            Some t =>
-              Thm {sign = sign, maxidx = maxidx_of_term t, hyps = [], prop = t}
+            Some t => Thm {sign = sign, maxidx = maxidx_of_term t,
+              shyps = [], hyps = [], prop = t}
           | None => get_ax parents handle Match => get_ax thys);
   in
     get_ax [theory] handle Match
@@ -431,12 +460,71 @@
 
 
 
-(**** Primitive rules ****)
+(*** Meta rules ***)
+
+(** sort contexts **)
+
+(*account for lost sort constraints*)
+fun fix_shyps ths Ts th =
+  let
+    fun thm_sorts (Thm {shyps, hyps, prop, ...}) =
+      unions (shyps :: term_sorts prop :: map term_sorts hyps);
+    val lost_sorts =
+      unions (map thm_sorts ths @ map typ_sorts Ts) \\ thm_sorts th;
+    val Thm {sign, maxidx, shyps, hyps, prop} = th;
+  in
+    Thm {sign = sign, maxidx = maxidx,
+      shyps = lost_sorts @ shyps, hyps = hyps, prop = prop}
+  end;
+
+(*remove sorts that are known to be non-empty (syntactically)*)
+val force_strip_shyps = ref true;  (* FIXME tmp *)
+fun strip_shyps th =
+  let
+    fun sort_hyps_of t =
+      term_tfrees t @ map (apfst Syntax.string_of_vname) (term_tvars t);
 
-(* discharge all assumptions t from ts *)
+    val Thm {sign, maxidx, shyps, hyps, prop} = th;
+    (* FIXME no varnames (?) *)
+    val sort_hyps = unions (sort_hyps_of prop :: map sort_hyps_of hyps);
+    (* FIXME improve (e.g. only minimal sorts) *)
+    val shyps' = filter_out (Sign.nonempty_sort sign sort_hyps) shyps;
+  in
+    Thm {sign = sign, maxidx = maxidx,
+      shyps =
+       (if null shyps' orelse not (! force_strip_shyps) then shyps'
+        else	(* FIXME tmp *)
+         (writeln ("WARNING Removed sort hypotheses: " ^
+           commas (map Type.str_of_sort shyps'));
+           writeln "WARNING Let's hope these sorts are non-empty!";
+           [])),
+      hyps = hyps, prop = prop}
+  end;
+
+(*discharge all sort hypotheses*)
+fun implies_intr_shyps (th as Thm {shyps = [], ...}) = th
+  | implies_intr_shyps (Thm {sign, maxidx, shyps, hyps, prop}) =
+      let
+        val used_names = foldr add_term_tfree_names (prop :: hyps, []);
+        val names =
+          tl (variantlist (replicate (length shyps + 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 = flat (map2 mk_insort (tfrees, shyps));
+      in
+        Thm {sign = sign, maxidx = maxidx, shyps = [],
+          hyps = hyps, prop = Logic.list_implies (sort_hyps, prop)}
+      end;
+
+
+
+(** 'primitive' rules **)
+
+(*discharge all assumptions t from ts*)
 val disch = gen_rem (op aconv);
 
-(*The assumption rule A|-A in a theory  *)
+(*The assumption rule A|-A in a theory*)
 fun assume ct : thm =
   let val {sign, t=prop, T, maxidx} = rep_cterm ct
   in  if T<>propT then
@@ -444,27 +532,29 @@
       else if maxidx <> ~1 then
         raise THM("assume: assumptions may not contain scheme variables",
                   maxidx, [])
-      else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop}
+      else Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop}
   end;
 
-(* Implication introduction
-              A |- B
-              -------
-              A ==> B    *)
-fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
+(*Implication introduction
+  A |- B
+  -------
+  A ==> B
+*)
+fun implies_intr cA (thB as Thm{sign,maxidx,shyps,hyps,prop}) : thm =
   let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
   in  if T<>propT then
         raise THM("implies_intr: assumptions must have type prop", 0, [thB])
       else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx],
-             hyps= disch(hyps,A),  prop= implies$A$prop}
+             shyps = shyps, hyps= disch(hyps,A),  prop= implies$A$prop}
       handle TERM _ =>
         raise THM("implies_intr: incompatible signatures", 0, [thB])
   end;
 
-(* Implication elimination
-        A ==> B       A
-        ---------------
-                B      *)
+(*Implication elimination
+  A ==> B    A
+  ------------
+        B
+*)
 fun implies_elim thAB thA : thm =
     let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA
         and Thm{sign, maxidx, hyps, prop,...} = thAB;
@@ -472,21 +562,24 @@
     in  case prop of
             imp$A$B =>
                 if imp=implies andalso  A aconv propA
-                then  Thm{sign= merge_thm_sgs(thAB,thA),
+                then fix_shyps [thAB, thA] []
+                       (Thm{sign= merge_thm_sgs(thAB,thA),
                           maxidx= max[maxA,maxidx],
+                          shyps= [],
                           hyps= hypsA union hyps,  (*dups suppressed*)
-                          prop= B}
+                          prop= B})
                 else err("major premise")
           | _ => err("major premise")
     end;
 
-(* Forall introduction.  The Free or Var x must not be free in the hypotheses.
-     A
-   ------
-   !!x.A       *)
-fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
+(*Forall introduction.  The Free or Var x must not be free in the hypotheses.
+    A
+  -----
+  !!x.A
+*)
+fun forall_intr cx (th as Thm{sign,maxidx,shyps,hyps,prop}) =
   let val x = term_of cx;
-      fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
+      fun result(a,T) = Thm{sign= sign, maxidx= maxidx, shyps= shyps, hyps= hyps,
                             prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   in  case x of
         Free(a,T) =>
@@ -497,30 +590,32 @@
       | _ => raise THM("forall_intr: not a variable", 0, [th])
   end;
 
-(* Forall elimination
-              !!x.A
-             --------
-              A[t/x]     *)
-fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
+(*Forall elimination
+  !!x.A
+  ------
+  A[t/x]
+*)
+fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop,...}) : thm =
   let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   in  case prop of
           Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
             if T<>qary then
                 raise THM("forall_elim: type mismatch", 0, [th])
-            else Thm{sign= Sign.merge(sign,signt),
+            else fix_shyps [th] []
+                 (Thm{sign= Sign.merge(sign,signt),
                      maxidx= max[maxidx, maxt],
-                     hyps= hyps,  prop= betapply(A,t)}
+                     shyps= [], hyps= hyps,  prop= betapply(A,t)})
         | _ => raise THM("forall_elim: not quantified", 0, [th])
   end
   handle TERM _ =>
          raise THM("forall_elim: incompatible signatures", 0, [th]);
 
 
-(*** Equality ***)
+(* Equality *)
 
-(*Definition of the relation =?= *)
+(* Definition of the relation =?= *)
 val flexpair_def =
-  Thm{sign= Sign.proto_pure, hyps= [], maxidx= 0,
+  Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0,
       prop= term_of
               (read_cterm Sign.proto_pure
                  ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
@@ -528,23 +623,26 @@
 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
 fun reflexive ct =
   let val {sign, t, T, maxidx} = rep_cterm ct
-  in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
+  in  Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx,
+        prop= Logic.mk_equals(t,t)}
   end;
 
 (*The symmetry rule
-    t==u
-    ----
-    u==t         *)
-fun symmetric (th as Thm{sign,hyps,prop,maxidx}) =
+  t==u
+  ----
+  u==t
+*)
+fun symmetric (th as Thm{sign,shyps,hyps,prop,maxidx}) =
   case prop of
       (eq as Const("==",_)) $ t $ u =>
-          Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t}
+          Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t}
     | _ => raise THM("symmetric", 0, [th]);
 
 (*The transitive rule
-    t1==u    u==t2
-    ------------
-        t1==t2      *)
+  t1==u    u==t2
+  --------------
+      t1==t2
+*)
 fun transitive th1 th2 =
   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
@@ -552,8 +650,10 @@
   in case (prop1,prop2) of
        ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
           if not (u aconv u') then err"middle term"  else
-              Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
-                  maxidx= max[max1,max2], prop= eq$t1$t2}
+              fix_shyps [th1, th2] []
+                (Thm{sign= merge_thm_sgs(th1,th2), shyps= [],
+                  hyps= hyps1 union hyps2,
+                  maxidx= max[max1,max2], prop= eq$t1$t2})
      | _ =>  err"premises"
   end;
 
@@ -562,17 +662,18 @@
   let val {sign, t, T, maxidx} = rep_cterm ct
   in  case t of
           Abs(_,_,bodt) $ u =>
-            Thm{sign= sign,  hyps= [],
+            Thm{sign= sign,  shyps= [], hyps= [],
                 maxidx= maxidx_of_term t,
                 prop= Logic.mk_equals(t, subst_bounds([u],bodt))}
         | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   end;
 
 (*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
-    f(x) == g(x)
-    ------------
-       f == g    *)
-fun extensional (th as Thm{sign,maxidx,hyps,prop}) =
+  f(x) == g(x)
+  ------------
+     f == g
+*)
+fun extensional (th as Thm{sign,maxidx,shyps,hyps,prop}) =
   case prop of
     (Const("==",_)) $ (f$x) $ (g$y) =>
       let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
@@ -585,23 +686,24 @@
                   if Logic.occs(y,f)  orelse  Logic.occs(y,g)
                   then err"variable free in functions"   else  ()
               | _ => err"not a variable");
-          Thm{sign=sign, hyps=hyps, maxidx=maxidx,
+          Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx,
               prop= Logic.mk_equals(f,g)}
       end
  | _ =>  raise THM("extensional: premise", 0, [th]);
 
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
-          t == u
-    ----------------
-      %(x)t == %(x)u     *)
-fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
+     t == u
+  ------------
+  %x.t == %x.u
+*)
+fun abstract_rule a cx (th as Thm{sign,maxidx,shyps,hyps,prop}) =
   let val x = term_of cx;
       val (t,u) = Logic.dest_equals prop
             handle TERM _ =>
                 raise THM("abstract_rule: premise not an equality", 0, [th])
       fun result T =
-            Thm{sign= sign, maxidx= maxidx, hyps= hyps,
+            Thm{sign= sign, maxidx= maxidx, shyps= shyps, hyps= hyps,
                 prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
                                       Abs(a, T, abstract_over (x,u)))}
   in  case x of
@@ -614,24 +716,27 @@
   end;
 
 (*The combination rule
-    f==g    t==u
-    ------------
-     f(t)==g(u)      *)
+  f==g    t==u
+  ------------
+   f(t)==g(u)
+*)
 fun combination th1 th2 =
-  let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
-      and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2
+  let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1
+      and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2
   in  case (prop1,prop2)  of
        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
-              Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
+              Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2,
+                  hyps= hyps1 union hyps2,
                   maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   end;
 
 
 (*The equal propositions rule
-    A==B    A
-    ---------
-        B          *)
+  A==B    A
+  ---------
+      B
+*)
 fun equal_elim th1 th2 =
   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
@@ -639,36 +744,42 @@
   in  case prop1  of
        Const("==",_) $ A $ B =>
           if not (prop2 aconv A) then err"not equal"  else
-              Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
-                  maxidx= max[max1,max2], prop= B}
+            fix_shyps [th1, th2] []
+              (Thm{sign= merge_thm_sgs(th1,th2), shyps= [],
+                  hyps= hyps1 union hyps2,
+                  maxidx= max[max1,max2], prop= B})
      | _ =>  err"major premise"
   end;
 
 
 (* Equality introduction
-    A==>B    B==>A
-    -------------
-         A==B            *)
+  A==>B    B==>A
+  --------------
+       A==B
+*)
 fun equal_intr th1 th2 =
-let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
-    and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
+let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1
+    and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2;
     fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
 in case (prop1,prop2) of
      (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
         if A aconv A' andalso B aconv B'
-        then Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
+        then Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2,
+                 hyps= hyps1 union hyps2,
                  maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}
         else err"not equal"
    | _ =>  err"premises"
 end;
 
+
+
 (**** Derived rules ****)
 
 (*Discharge all hypotheses (need not verify cterms)
   Repeated hypotheses are discharged only once;  fold cannot do this*)
-fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) =
+fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) =
       implies_intr_hyps
-            (Thm{sign=sign,  maxidx=maxidx,
+            (Thm{sign=sign,  maxidx=maxidx, shyps=shyps,
                  hyps= disch(As,A),  prop= implies$A$prop})
   | implies_intr_hyps th = th;
 
@@ -676,15 +787,16 @@
   Instantiates the theorem and deletes trivial tpairs.
   Resulting sequence may contain multiple elements if the tpairs are
     not all flex-flex. *)
-fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) =
+fun flexflex_rule (th as Thm{sign,maxidx,hyps,prop,...}) =
   let fun newthm env =
           let val (tpairs,horn) =
                         Logic.strip_flexpairs (Envir.norm_term env prop)
                 (*Remove trivial tpairs, of the form t=t*)
               val distpairs = filter (not o op aconv) tpairs
               val newprop = Logic.list_flexpairs(distpairs, horn)
-          in  Thm{sign= sign, hyps= hyps,
-                  maxidx= maxidx_of_term newprop, prop= newprop}
+          in  fix_shyps [th] (env_codT env)
+                (Thm{sign= sign, shyps= [], hyps= hyps,
+                  maxidx= maxidx_of_term newprop, prop= newprop})
           end;
       val (tpairs,_) = Logic.strip_flexpairs prop
   in Sequence.maps newthm
@@ -692,9 +804,10 @@
   end;
 
 (*Instantiation of Vars
-                      A
-             --------------------
-              A[t1/v1,....,tn/vn]     *)
+           A
+  -------------------
+  A[t1/v1,....,tn/vn]
+*)
 
 (*Check that all the terms are Vars and are distinct*)
 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
@@ -714,15 +827,17 @@
 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   Instantiates distinct Vars by terms of same type.
   Normalizes the new theorem! *)
-fun instantiate (vcTs,ctpairs)  (th as Thm{sign,maxidx,hyps,prop}) =
+fun instantiate (vcTs,ctpairs)  (th as Thm{sign,maxidx,hyps,prop,...}) =
   let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
       val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
       val newprop =
             Envir.norm_term (Envir.empty 0)
               (subst_atomic tpairs
                (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop))
-      val newth = Thm{sign= newsign, hyps= hyps,
-                      maxidx= maxidx_of_term newprop, prop= newprop}
+      val newth =
+            fix_shyps [th] (map snd vTs)
+              (Thm{sign= newsign, shyps= [], hyps= hyps,
+                maxidx= maxidx_of_term newprop, prop= newprop})
   in  if not(instl_ok(map #1 tpairs))
       then raise THM("instantiate: variables not distinct", 0, [th])
       else if not(null(findrep(map #1 vTs)))
@@ -748,11 +863,12 @@
   let val {sign, t=A, T, maxidx} = rep_cterm ct
   in  if T<>propT then
             raise THM("trivial: the term must have type prop", 0, [])
-      else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
+      else Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [],
+             prop= implies$A$A}
   end;
 
 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" --
-  essentially an instance of A==>A.*)
+  essentially just an instance of A==>A.*)
 fun class_triv thy c =
   let
     val sign = sign_of thy;
@@ -760,21 +876,23 @@
       cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
         handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   in
-    Thm {sign = sign, maxidx = maxidx, hyps = [], prop = t}
+    Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}
   end;
 
 
 (* Replace all TFrees not in the hyps by new TVars *)
-fun varifyT(Thm{sign,maxidx,hyps,prop}) =
+fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) =
   let val tfrees = foldr add_term_tfree_names (hyps,[])
-  in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps,
+  in Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps,
          prop= Type.varify(prop,tfrees)}
   end;
 
 (* Replace all TVars by new TFrees *)
-fun freezeT(Thm{sign,maxidx,hyps,prop}) =
+fun freezeT(Thm{sign,maxidx,shyps,hyps,prop}) =
   let val prop' = Type.freeze prop
-  in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;
+  in Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps,
+       prop=prop'}
+  end;
 
 
 (*** Inference rules for tactics ***)
@@ -795,24 +913,26 @@
       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
         handle TERM _ => raise THM("lift_rule", i, [orule,state]);
       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1);
-      val (Thm{sign,maxidx,hyps,prop}) = orule
+      val (Thm{sign,maxidx,hyps,prop,...}) = orule
       val (tpairs,As,B) = Logic.strip_horn prop
-  in  Thm{hyps=hyps, sign= merge_thm_sgs(state,orule),
-          maxidx= maxidx+smax+1,
+  in  fix_shyps [state, orule] []
+        (Thm{hyps=hyps, sign= merge_thm_sgs(state,orule),
+          shyps=[], maxidx= maxidx+smax+1,
           prop= Logic.rule_of(map (pairself lift_abs) tpairs,
-                              map lift_all As,    lift_all B)}
+                              map lift_all As,    lift_all B)})
   end;
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
 fun assumption i state =
-  let val Thm{sign,maxidx,hyps,prop} = state;
+  let val Thm{sign,maxidx,hyps,prop,...} = state;
       val (tpairs, Bs, Bi, C) = dest_state(state,i)
       fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
-          Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
+        fix_shyps [state] (env_codT env)
+          (Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop=
             if Envir.is_empty env then (*avoid wasted normalizations*)
               Logic.rule_of (tpairs, Bs, C)
             else (*normalize the new rule fully*)
-              Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))};
+              Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
       fun addprfs [] = Sequence.null
         | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
              (Sequence.mapp newth
@@ -823,11 +943,12 @@
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
 fun eq_assumption i state =
-  let val Thm{sign,maxidx,hyps,prop} = state;
+  let val Thm{sign,maxidx,hyps,prop,...} = state;
       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   in  if exists (op aconv) (Logic.assum_pairs Bi)
-      then Thm{sign=sign, hyps=hyps, maxidx=maxidx,
-               prop=Logic.rule_of(tpairs, Bs, C)}
+      then fix_shyps [state] []
+             (Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx,
+               prop=Logic.rule_of(tpairs, Bs, C)})
       else  raise THM("eq_assumption", 0, [state])
   end;
 
@@ -839,7 +960,7 @@
   The names in cs, if distinct, are used for the innermost parameters;
    preceding parameters may be renamed to make all params distinct.*)
 fun rename_params_rule (cs, i) state =
-  let val Thm{sign,maxidx,hyps,prop} = state
+  let val Thm{sign,maxidx,hyps,prop,...} = state
       val (tpairs, Bs, Bi, C) = dest_state(state,i)
       val iparams = map #1 (Logic.strip_params Bi)
       val short = length iparams - length cs
@@ -853,8 +974,9 @@
      c::_ => error ("Bound variables not distinct: " ^ c)
    | [] => (case cs inter freenames of
        a::_ => error ("Bound/Free variable clash: " ^ a)
-     | [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
-                    Logic.rule_of(tpairs, Bs@[newBi], C)})
+     | [] => fix_shyps [state] []
+               (Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop=
+                 Logic.rule_of(tpairs, Bs@[newBi], C)}))
   end;
 
 (*** Preservation of bound variable names ***)
@@ -971,8 +1093,10 @@
                 else (*normalize the new rule fully*)
                   (ntps, map normt (Bs @ As), normt C)
              end
-           val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx,
-                        prop= Logic.rule_of normp}
+           val th =
+             fix_shyps [state, orule] (env_codT env)
+               (Thm{sign=sign, shyps=[], hyps=rhyps union shyps,
+                 maxidx=maxidx, prop= Logic.rule_of normp})
         in  cons(th, thq)  end  handle Bicompose => thq
      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
@@ -1092,7 +1216,7 @@
    ?m < ?n ==> f(?n) == f(?m)
 *)
 
-fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
+fun mk_rrule (thm as Thm{sign,prop,maxidx,...}) =
   let val prems = Logic.strip_imp_prems prop
       val concl = Logic.strip_imp_concl prop
       val (lhs,_) = Logic.dest_equals concl handle TERM _ =>
@@ -1101,8 +1225,11 @@
       val (elhs,erhs) = Logic.dest_equals econcl
       val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs)
                                      andalso not(is_Var(elhs))
-  in if not perm andalso loops sign prems (elhs,erhs)
-     then (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
+  in
+     if not (null (#shyps (rep_thm (strip_shyps thm)))) then     (* FIXME tmp hack *)
+       raise SIMPLIFIER ("Rewrite rule may not contain sort hypotheses", thm)
+     else if not perm andalso loops sign prems (elhs,erhs) then
+       (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
      else Some{thm=thm,lhs=lhs,perm=perm}
   end;
 
@@ -1256,7 +1383,9 @@
             val prop' = ren_inst(insts,rprop,rlhs,t);
             val hyps' = hyps union hypst;
             val maxidx' = maxidx_of_term prop'
-            val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx'}
+            val thm' = fix_shyps [thm] []       (* FIXME ??? *)
+                         (Thm{sign=signt, shyps=[], hyps=hyps',
+                           prop=prop', maxidx=maxidx'})
             val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
         in if perm andalso not(termless(rhs',lhs')) then None else
            if Logic.count_prems(prop',0) = 0
@@ -1290,8 +1419,9 @@
       val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH =>
                   error("Congruence rule did not match")
       val prop' = ren_inst(insts,rprop,rlhs,t);
-      val thm' = Thm{sign=signt, hyps=hyps union hypst,
-                     prop=prop', maxidx=maxidx_of_term prop'}
+      val thm' = fix_shyps [cong] []      (* FIXME ??? *)
+                   (Thm{sign=signt, shyps=[], hyps=hyps union hypst,
+                     prop=prop', maxidx=maxidx_of_term prop'})
       val unit = trace_thm "Applying congruence rule" thm';
       fun err() = error("Failed congruence proof!")
 
@@ -1370,7 +1500,7 @@
             val maxidx1 = maxidx_of_term s1
             val mss1 =
               if not useprem orelse maxidx1 <> ~1 then mss
-              else let val thm = Thm{sign=sign,hyps=[s1],prop=s1,maxidx= ~1}
+              else let val thm = Thm{sign=sign,shyps=[],hyps=[s1],prop=s1,maxidx= ~1}
                    in add_simps(add_prems(mss,[thm]), mk_rews thm) end
             val (hyps2,maxidx2,u1) = try_botc mss1 (hyps1,maxidx,u)
             val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1
@@ -1385,13 +1515,14 @@
    mss: contains equality theorems of the form [|p1,...|] ==> t==u
    prover: how to solve premises in conditional rewrites and congruences
 *)
-
+(* FIXME: better handling of shyps *)
 (*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***)
 fun rewrite_cterm mode mss prover ct =
   let val {sign, t, T, maxidx} = rep_cterm ct;
       val (hyps,maxidxu,u) = bottomc (mode,prover,sign) mss ([],maxidx,t);
       val prop = Logic.mk_equals(t,u)
-  in  Thm{sign= sign, hyps= hyps, maxidx= max[maxidx,maxidxu], prop= prop}
+  in  Thm{sign= sign, shyps=[], hyps= hyps, maxidx= max[maxidx,maxidxu],
+        prop= prop}
   end
 
 end;