src/Pure/thm.ML

 simplification).
 *)
 
 signature THM =
 sig
-  structure Envir 	: ENVIR
-  structure Sequence 	: SEQUENCE
-  structure Sign 	: SIGN
+  structure Envir       : ENVIR
+  structure Sequence    : SEQUENCE
+  structure Sign        : SIGN
 
   (*certified types*)
   type ctyp
-  val rep_ctyp		: ctyp -> {sign: Sign.sg, T: typ}
-  val typ_of		: ctyp -> typ
-  val ctyp_of		: Sign.sg -> typ -> ctyp
-  val read_ctyp		: Sign.sg -> string -> ctyp
+  val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
+  val typ_of            : ctyp -> typ
+  val ctyp_of           : Sign.sg -> typ -> ctyp
+  val read_ctyp         : Sign.sg -> string -> ctyp
 
   (*certified terms*)
   type cterm
-  val rep_cterm		: cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
-  val term_of		: cterm -> term
-  val cterm_of		: Sign.sg -> term -> cterm
-  val read_cterm	: Sign.sg -> string * typ -> cterm
-  val cterm_fun		: (term -> term) -> (cterm -> cterm)
-  val dest_cimplies	: cterm -> cterm * cterm
-  val read_def_cterm 	:
+  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
+  val term_of           : cterm -> term
+  val cterm_of          : Sign.sg -> term -> cterm
+  val read_cterm        : Sign.sg -> string * typ -> cterm
+  val cterm_fun         : (term -> term) -> (cterm -> cterm)
+  val dest_cimplies     : cterm -> cterm * cterm
+  val read_def_cterm    :
     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> string * typ -> cterm * (indexname * typ) list
 
   (*meta theorems*)
   type thm
   exception THM of string * int * thm list
-  val rep_thm		: thm -> {sign: Sign.sg, maxidx: int,
+  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
-  val nprems_of		: thm -> int
-  val concl_of		: thm -> term
-  val cprop_of		: thm -> cterm
-  val cert_axm		: Sign.sg -> string * term -> string * term
-  val read_axm		: Sign.sg -> string * string -> string * term
-  val inferT_axm	: Sign.sg -> string * term -> string * term
+  val stamps_of_thm     : thm -> string ref list
+  val tpairs_of         : thm -> (term * term) list
+  val prems_of          : thm -> term list
+  val nprems_of         : thm -> int
+  val concl_of          : thm -> term
+  val cprop_of          : thm -> cterm
+  val extra_shyps       : thm -> sort list
+  val force_strip_shyps : bool ref      (* FIXME tmp *)
+  val strip_shyps       : thm -> thm
+  val implies_intr_shyps: thm -> thm
+  val cert_axm          : Sign.sg -> string * term -> string * term
+  val read_axm          : Sign.sg -> string * string -> string * term
+  val inferT_axm        : Sign.sg -> string * term -> string * term
 
   (*theories*)
   type theory
   exception THEORY of string * theory list
-  val rep_theory	: theory ->
+  val rep_theory        : theory ->
     {sign: Sign.sg, new_axioms: term Sign.Symtab.table, parents: theory list}
-  val sign_of		: theory -> Sign.sg
-  val syn_of		: theory -> Sign.Syntax.syntax
-  val stamps_of_thy	: theory -> string ref list
-  val parents_of	: theory -> theory list
-  val subthy		: theory * theory -> bool
-  val eq_thy		: theory * theory -> bool
-  val get_axiom		: theory -> string -> thm
-  val axioms_of		: theory -> (string * thm) list
-  val proto_pure_thy	: theory
-  val pure_thy		: theory
-  val cpure_thy		: theory
+  val sign_of           : theory -> Sign.sg
+  val syn_of            : theory -> Sign.Syntax.syntax
+  val stamps_of_thy     : theory -> string ref list
+  val parents_of        : theory -> theory list
+  val subthy            : theory * theory -> bool
+  val eq_thy            : theory * theory -> bool
+  val get_axiom         : theory -> string -> thm
+  val axioms_of         : theory -> (string * thm) list
+  val proto_pure_thy    : theory
+  val pure_thy          : theory
+  val cpure_thy         : theory
   local open Sign.Syntax in
-    val add_classes	: (class * class list) list -> theory -> theory
-    val add_classrel	: (class * class) list -> theory -> theory
-    val add_defsort	: sort -> theory -> theory
-    val add_types	: (string * int * mixfix) list -> theory -> theory
-    val add_tyabbrs	: (string * string list * string * mixfix) list
+    val add_classes     : (class * class list) list -> theory -> theory
+    val add_classrel    : (class * class) list -> theory -> theory
+    val add_defsort     : sort -> theory -> theory
+    val add_types       : (string * int * mixfix) list -> theory -> theory
+    val add_tyabbrs     : (string * string list * string * mixfix) list
       -> theory -> theory
-    val add_tyabbrs_i	: (string * string list * typ * mixfix) list
+    val add_tyabbrs_i   : (string * string list * typ * mixfix) list
       -> theory -> theory
-    val add_arities	: (string * sort list * sort) list -> theory -> theory
-    val add_consts	: (string * string * mixfix) list -> theory -> theory
-    val add_consts_i	: (string * typ * mixfix) list -> theory -> theory
-    val add_syntax	: (string * string * mixfix) list -> theory -> theory
-    val add_syntax_i	: (string * typ * mixfix) list -> theory -> theory
-    val add_trfuns	:
+    val add_arities     : (string * sort list * sort) list -> theory -> theory
+    val add_consts      : (string * string * mixfix) list -> theory -> theory
+    val add_consts_i    : (string * typ * mixfix) list -> theory -> theory
+    val add_syntax      : (string * string * mixfix) list -> theory -> theory
+    val add_syntax_i    : (string * typ * mixfix) list -> theory -> theory
+    val add_trfuns      :
       (string * (ast list -> ast)) list *
       (string * (term list -> term)) list *
       (string * (term list -> term)) list *
       (string * (ast list -> ast)) list -> theory -> theory
-    val add_trrules	: (string * string) trrule list -> theory -> theory
-    val add_trrules_i	: ast trrule list -> theory -> theory
-    val add_axioms	: (string * string) list -> theory -> theory
-    val add_axioms_i	: (string * term) list -> theory -> theory
-    val add_thyname	: string -> theory -> theory
+    val add_trrules     : (string * string) trrule list -> theory -> theory
+    val add_trrules_i   : ast trrule list -> theory -> theory
+    val add_axioms      : (string * string) list -> theory -> theory
+    val add_axioms_i    : (string * term) list -> theory -> theory
+    val add_thyname     : string -> theory -> theory
   end
-  val merge_theories	: theory * theory -> theory
-  val merge_thy_list	: bool -> theory list -> theory
+  val merge_theories    : theory * theory -> theory
+  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
-  val forall_intr	: cterm -> thm -> thm
-  val forall_elim	: cterm -> thm -> thm
-  val flexpair_def	: thm
-  val reflexive		: cterm -> thm
-  val symmetric		: thm -> thm
-  val transitive	: thm -> thm -> thm
-  val beta_conversion	: cterm -> thm
-  val extensional	: thm -> thm
-  val abstract_rule	: string -> cterm -> thm -> thm
-  val combination	: thm -> thm -> thm
-  val equal_intr	: thm -> thm -> thm
-  val equal_elim	: thm -> thm -> thm
-  val implies_intr_hyps	: thm -> thm
-  val flexflex_rule	: thm -> thm Sequence.seq
-  val instantiate	:
+  val assume            : cterm -> thm
+  val implies_intr      : cterm -> thm -> thm
+  val implies_elim      : thm -> thm -> thm
+  val forall_intr       : cterm -> thm -> thm
+  val forall_elim       : cterm -> thm -> thm
+  val flexpair_def      : thm
+  val reflexive         : cterm -> thm
+  val symmetric         : thm -> thm
+  val transitive        : thm -> thm -> thm
+  val beta_conversion   : cterm -> thm
+  val extensional       : thm -> thm
+  val abstract_rule     : string -> cterm -> thm -> thm
+  val combination       : thm -> thm -> thm
+  val equal_intr        : thm -> thm -> thm
+  val equal_elim        : thm -> thm -> thm
+  val implies_intr_hyps : thm -> thm
+  val flexflex_rule     : thm -> thm Sequence.seq
+  val instantiate       :
     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
-  val trivial		: cterm -> thm
-  val class_triv	: theory -> class -> thm
-  val varifyT		: thm -> thm
-  val freezeT		: thm -> thm
-  val dest_state	: thm * int ->
+  val trivial           : cterm -> thm
+  val class_triv        : theory -> class -> thm
+  val varifyT           : thm -> thm
+  val freezeT           : thm -> thm
+  val dest_state        : thm * int ->
     (term * term) list * term list * term * term
-  val lift_rule		: (thm * int) -> thm -> thm
-  val assumption	: int -> thm -> thm Sequence.seq
-  val eq_assumption	: int -> thm -> thm
+  val lift_rule         : (thm * int) -> thm -> thm
+  val assumption        : int -> thm -> thm Sequence.seq
+  val eq_assumption     : int -> thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
-  val bicompose		: bool -> bool * thm * int ->
+  val bicompose         : bool -> bool * thm * int ->
     int -> thm -> thm Sequence.seq
-  val biresolution	: bool -> (bool * thm) list ->
+  val biresolution      : bool -> (bool * thm) list ->
     int -> thm -> thm Sequence.seq
 
   (*meta simplification*)
   type meta_simpset
   exception SIMPLIFIER of string * thm
-  val empty_mss		: meta_simpset
-  val add_simps		: meta_simpset * thm list -> meta_simpset
-  val del_simps		: meta_simpset * thm list -> meta_simpset
-  val mss_of		: thm list -> meta_simpset
-  val add_congs		: meta_simpset * thm list -> meta_simpset
-  val add_prems		: meta_simpset * thm list -> meta_simpset
-  val prems_of_mss	: meta_simpset -> thm list
-  val set_mk_rews	: meta_simpset * (thm -> thm list) -> meta_simpset
-  val mk_rews_of_mss	: meta_simpset -> thm -> thm list
-  val trace_simp	: bool ref
-  val rewrite_cterm	: bool * bool -> meta_simpset ->
+  val empty_mss         : meta_simpset
+  val add_simps         : meta_simpset * thm list -> meta_simpset
+  val del_simps         : meta_simpset * thm list -> meta_simpset
+  val mss_of            : thm list -> meta_simpset
+  val add_congs         : meta_simpset * thm list -> meta_simpset
+  val add_prems         : meta_simpset * thm list -> meta_simpset
+  val prems_of_mss      : meta_simpset -> thm list
+  val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
+  val mk_rews_of_mss    : meta_simpset -> thm -> thm list
+  val trace_simp        : bool ref
+  val rewrite_cterm     : bool * bool -> meta_simpset ->
     (meta_simpset -> thm -> thm option) -> cterm -> thm
 end;
 
 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN
   and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM =

 
 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
 
 
 
-(* 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 ***)
 
+(* FIXME comment *)
 datatype thm = Thm of
   {sign: Sign.sg, maxidx: int,
     shyps: sort list, hyps: term list, prop: term};
 
 fun rep_thm (Thm args) = args;

 fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
 
 (*the statement of any thm is a cterm*)
 fun cprop_of (Thm {sign, maxidx, prop, ...}) =
   Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop};
+
+
+
+(** sort contexts of theorems **)
+
+(* basic utils *)
+
+(*accumulate sorts suppressing duplicates; these are coded low level
+  to improve efficiency a bit*)
+
+fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
+  | add_typ_sorts (TFree (_, S), Ss) = S ins Ss
+  | add_typ_sorts (TVar (_, S), Ss) = S ins Ss
+and add_typs_sorts ([], Ss) = Ss
+  | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
+
+fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
+  | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
+  | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
+  | add_term_sorts (Bound _, Ss) = Ss
+  | add_term_sorts (Abs (_, T, t), Ss) = add_term_sorts (t, add_typ_sorts (T, Ss))
+  | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));
+
+fun add_terms_sorts ([], Ss) = Ss
+  | add_terms_sorts (t :: ts, Ss) = add_terms_sorts (ts, add_term_sorts (t, Ss));
+
+fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
+  add_terms_sorts (hyps, add_term_sorts (prop, Ss));
+
+fun add_thms_shyps ([], Ss) = Ss
+  | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
+      add_thms_shyps (ths, shyps union Ss);
+
+
+(*get 'dangling' sort constraints of a thm*)
+fun extra_shyps (th as Thm {shyps, ...}) =
+  shyps \\ add_thm_sorts (th, []);
+
+
+(* fix_shyps *)
+
+(*preserve sort contexts of rule premises and substituted types*)
+fun fix_shyps thms Ts thm =
+  let
+    val Thm {sign, maxidx, hyps, prop, ...} = thm;
+    val shyps =
+      add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
+  in
+    Thm {sign = sign, maxidx = maxidx,
+      shyps = shyps, hyps = hyps, prop = prop}
+  end;
+
+fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
+
+
+(* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
+
+val force_strip_shyps = ref true;  (* FIXME tmp *)
+
+(*remove extra sorts that are known to be syntactically non-empty*)
+fun strip_shyps thm =
+  let
+    val Thm {sign, maxidx, shyps, hyps, prop} = thm;
+    val sorts = add_thm_sorts (thm, []);
+    val maybe_empty = not o Sign.nonempty_sort sign sorts;
+    val shyps' = filter (fn S => S mem sorts orelse maybe_empty S) shyps;
+  in
+    Thm {sign = sign, maxidx = maxidx,
+      shyps =
+       (if eq_set (shyps', sorts) orelse not (! force_strip_shyps) then shyps'
+        else    (* FIXME tmp *)
+         (writeln ("WARNING Removed sort hypotheses: " ^
+           commas (map Type.str_of_sort (shyps' \\ sorts)));
+           writeln "WARNING Let's hope these sorts are non-empty!";
+           sorts)),
+      hyps = hyps, prop = prop}
+  end;
+
+
+(* implies_intr_shyps *)
+
+(*discharge all extra sort hypotheses*)
+fun implies_intr_shyps thm =
+  (case extra_shyps thm of
+    [] => thm
+  | xshyps =>
+      let
+        val Thm {sign, maxidx, shyps, hyps, prop} = thm;
+        val shyps' = logicS ins (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 = flat (map2 mk_insort (tfrees, xshyps));
+      in
+        Thm {sign = sign, maxidx = maxidx, shyps = shyps',
+          hyps = hyps, prop = Logic.list_implies (sort_hyps, prop)}
+      end);
 
 
 
 (*** Theories ***)
 

 fun get_axiom theory name =
   let
     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,
-              shyps = [], hyps = [], prop = t}
+            Some t => fix_shyps [] []
+              (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
       => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory])
   end;

 
 
 
 (*** Meta rules ***)
 
-(** sort contexts **)
-
-(*account for lost sort constraints*)
-fun fix_shyps ths Ts th = th;
-(* FIXME
-  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);
-
-    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);
 

   in  if T<>propT then
         raise THM("assume: assumptions must have type prop", 0, [])
       else if maxidx <> ~1 then
         raise THM("assume: assumptions may not contain scheme variables",
                   maxidx, [])
-      else Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop}
+      else fix_shyps [] []
+        (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,shyps,hyps,prop}) : thm =
+fun implies_intr cA (thB as Thm{sign,maxidx,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],
-             shyps = shyps, hyps= disch(hyps,A),  prop= implies$A$prop}
+      else fix_shyps [thB] []
+        (Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx],
+          shyps= [], hyps= disch(hyps,A),  prop= implies$A$prop})
       handle TERM _ =>
         raise THM("implies_intr: incompatible signatures", 0, [thB])
   end;
 
 (*Implication elimination

 (*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}) =
+fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop,...}) =
   let val x = term_of cx;
-      fun result(a,T) = Thm{sign= sign, maxidx= maxidx, shyps= shyps, hyps= hyps,
-                            prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
+      fun result(a,T) = fix_shyps [th] []
+        (Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps,
+          prop= all(T) $ Abs(a, T, abstract_over (x,prop))})
   in  case x of
         Free(a,T) =>
           if exists (apl(x, Logic.occs)) hyps
           then  raise THM("forall_intr: variable free in assumptions", 0, [th])
           else  result(a,T)

 
 
 (* Equality *)
 
 (* Definition of the relation =?= *)
-val flexpair_def =
-  Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0,
-      prop= term_of
-              (read_cterm Sign.proto_pure
-                 ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
+val flexpair_def = fix_shyps [] []
+  (Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0,
+        prop= term_of (read_cterm Sign.proto_pure
+                ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
 
 (*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, shyps= [], hyps= [], maxidx= maxidx,
-        prop= Logic.mk_equals(t,t)}
+  in  fix_shyps [] []
+       (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,shyps,hyps,prop,maxidx}) =
   case prop of
       (eq as Const("==",_)) $ t $ u =>
-          Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t}
+        (*no fix_shyps*)
+        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
   --------------

 
 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
 fun beta_conversion ct =
   let val {sign, t, T, maxidx} = rep_cterm ct
   in  case t of
-          Abs(_,_,bodt) $ u =>
-            Thm{sign= sign,  shyps= [], hyps= [],
+          Abs(_,_,bodt) $ u => fix_shyps [] []
+            (Thm{sign= sign,  shyps= [], hyps= [],
                 maxidx= maxidx_of_term t,
-                prop= Logic.mk_equals(t, subst_bounds([u],bodt))}
+                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)

                   then err"variable free in hyps or functions"    else  ()
               | Var _ =>
                   if Logic.occs(y,f)  orelse  Logic.occs(y,g)
                   then err"variable free in functions"   else  ()
               | _ => err"not a variable");
+          (*no fix_shyps*)
           Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx,
               prop= Logic.mk_equals(f,g)}
       end
  | _ =>  raise THM("extensional: premise", 0, [th]);
 

   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,shyps,hyps,prop}) =
+fun abstract_rule a cx (th as Thm{sign,maxidx,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, shyps= shyps, hyps= hyps,
+      fun result T = fix_shyps [th] []
+            (Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps,
                 prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
-                                      Abs(a, T, abstract_over (x,u)))}
+                                      Abs(a, T, abstract_over (x,u)))})
   in  case x of
         Free(_,T) =>
          if exists (apl(x, Logic.occs)) hyps
          then raise THM("abstract_rule: variable free in assumptions", 0, [th])
          else result T

 fun combination th1 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) =>
+              (*no fix_shyps*)
               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;

     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), shyps= shyps1 union shyps2,
-                 hyps= hyps1 union hyps2,
-                 maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}
+        then
+          (*no fix_shyps*)
+          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, shyps, hyps=A::As, prop}) =
-      implies_intr_hyps
+      implies_intr_hyps (*no fix_shyps*)
             (Thm{sign=sign,  maxidx=maxidx, shyps=shyps,
                  hyps= disch(As,A),  prop= implies$A$prop})
   | implies_intr_hyps th = th;
 
 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.

   A can contain Vars, not so for assume!   *)
 fun trivial ct : thm =
   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, shyps= [], hyps= [],
-             prop= implies$A$A}
+      else fix_shyps [] []
+        (Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [],
+              prop= implies$A$A})
   end;
 
 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" --
   essentially just an instance of A==>A.*)
 fun class_triv thy c =

     val sign = sign_of thy;
     val Cterm {t, maxidx, ...} =
       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, shyps = [], hyps = [], prop = t}
+    fix_shyps [] []
+      (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,shyps,hyps,prop}) =
   let val tfrees = foldr add_term_tfree_names (hyps,[])
-  in Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps,
-         prop= Type.varify(prop,tfrees)}
+  in (*no fix_shyps*)
+    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,shyps,hyps,prop}) =
   let val prop' = Type.freeze prop
-  in Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps,
-       prop=prop'}
+  in (*no fix_shyps*)
+    Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps,
+        prop=prop'}
   end;
 
 
 (*** Inference rules for tactics ***)
 

   handle TERM _ => raise THM("dest_state", i, [state]);
 
 (*Increment variables and parameters of orule as required for
   resolution with goal i of state. *)
 fun lift_rule (state, i) orule =
-  let val Thm{prop=sprop,maxidx=smax,...} = state;
+  let val Thm{shyps=sshyps,prop=sprop,maxidx=smax,...} = state;
       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,shyps,hyps,prop}) = orule
       val (tpairs,As,B) = Logic.strip_horn prop
-  in  fix_shyps [state, orule] []
-        (Thm{hyps=hyps, sign= merge_thm_sgs(state,orule),
-          shyps=[], maxidx= maxidx+smax+1,
+  in  (*no fix_shyps*)
+      Thm{hyps=hyps, sign= merge_thm_sgs(state,orule),
+          shyps=sshyps union 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;

 
 (*** Preservation of bound variable names ***)
 
 (*Scan a pair of terms; while they are similar,
   accumulate corresponding bound vars in "al"*)
-fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
+fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
       match_bvs(s, t, if x="" orelse y="" then al
-		                          else (x,y)::al)
+                                          else (x,y)::al)
   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   | match_bvs(_,_,al) = al;
 
 (* strip abstractions created by parameters *)
 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);

 
 (*Faster normalization: skip assumptions that were lifted over*)
 fun norm_term_skip env 0 t = Envir.norm_term env t
   | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
         let val Envir.Envir{iTs, ...} = env
-	    val T' = typ_subst_TVars iTs T
-	    (*Must instantiate types of parameters because they are flattened;
+            val T' = typ_subst_TVars iTs T
+            (*Must instantiate types of parameters because they are flattened;
               this could be a NEW parameter*)
         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
   | norm_term_skip env n (Const("==>", _) $ A $ B) =
-	implies $ A $ norm_term_skip env (n-1) B
+        implies $ A $ norm_term_skip env (n-1) B
   | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
 
 
 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)

 in
 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
                         (eres_flg, orule, nsubgoal) =
  let val Thm{maxidx=smax, hyps=shyps, ...} = state
      and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule
-	     (*How many hyps to skip over during normalization*)
-     and nlift = Logic.count_prems(strip_all_body Bi, 
-				   if eres_flg then ~1 else 0)
+             (*How many hyps to skip over during normalization*)
+     and nlift = Logic.count_prems(strip_all_body Bi,
+                                   if eres_flg then ~1 else 0)
      val sign = merge_thm_sgs(state,orule);
      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
      fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
        let val normt = Envir.norm_term env;
            (*perform minimal copying here by examining env*)
            val normp =
              if Envir.is_empty env then (tpairs, Bs @ As, C)
              else
              let val ntps = map (pairself normt) tpairs
-             in if the (Envir.minidx env) > smax then 
-		  (*no assignments in state; normalize the rule only*)
-                  if lifted 
-		  then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
-		  else (ntps, Bs @ map normt As, C)
+             in if the (Envir.minidx env) > smax then
+                  (*no assignments in state; normalize the rule only*)
+                  if lifted
+                  then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
+                  else (ntps, Bs @ map normt As, C)
                 else if match then raise Bicompose
                 else (*normalize the new rule fully*)
                   (ntps, map normt (Bs @ As), normt C)
              end
-           val th =
+           val th = (* FIXME improve *)
              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);

    conditional rewrites with extra variables in the conditions may terminate
    although the rhs is an instance of the lhs. Example:
    ?m < ?n ==> f(?n) == f(?m)
 *)
 
-fun mk_rrule (thm as Thm{sign,prop,maxidx,...}) =
-  let val prems = Logic.strip_imp_prems prop
+fun mk_rrule raw_thm =
+  let
+      val thm = strip_shyps raw_thm;            (* FIXME tmp *)
+      val Thm{sign,prop,maxidx,...} = thm;
+      val prems = Logic.strip_imp_prems prop
       val concl = Logic.strip_imp_concl prop
       val (lhs,_) = Logic.dest_equals concl handle TERM _ =>
                       raise SIMPLIFIER("Rewrite rule not a meta-equality",thm)
       val econcl = Pattern.eta_contract concl
       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 (null (#shyps (rep_thm (strip_shyps thm)))) then     (* FIXME tmp hack *)
-       raise SIMPLIFIER ("Rewrite rule may not contain sort hypotheses", thm)
+     if not (null (extra_shyps thm)) then     (* FIXME tmp *)
+       raise SIMPLIFIER ("Rewrite rule may not contain extra 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;
 

         let val (hyps1,_,s1) = if simprem then try_botc mss (hyps,maxidx,s)
                                else (hyps,0,s);
             val maxidx1 = maxidx_of_term s1
             val mss1 =
               if not useprem orelse maxidx1 <> ~1 then mss
-              else let val thm = Thm{sign=sign,shyps=[],hyps=[s1],prop=s1,maxidx= ~1}
+              else let val thm = fix_shyps [] []        (* FIXME ??? *)
+                     (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
         in (hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end
 

 (*** 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, shyps=[], hyps= hyps, maxidx= max[maxidx,maxidxu],
-        prop= prop}
+  in  fix_shyps [] []
+       (Thm{sign= sign, shyps=[], hyps= hyps, maxidx= max[maxidx,maxidxu],
+         prop= prop})
   end
 
 end;
-