more efficient treatment of shyps and hyps (use ordered lists);
authorwenzelm
Wed Jun 29 15:13:31 2005 +0200 (2005-06-29)
changeset 16601ee8eefade568
parent 16600 55ffcee3b8f3
child 16602 0eda2f8a74aa
more efficient treatment of shyps and hyps (use ordered lists);
added 'sorts' field to cterm;
removed obsolete fix_shyps;
moved implies_intr_hyps to drule.ML;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed Jun 29 15:13:30 2005 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Jun 29 15:13:31 2005 +0200
     1.3 @@ -20,8 +20,10 @@
     1.4    (*certified terms*)
     1.5    type cterm
     1.6    exception CTERM of string
     1.7 -  val rep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: typ, maxidx: int}
     1.8 -  val crep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int}
     1.9 +  val rep_cterm: cterm ->
    1.10 +    {thy: theory, sign: theory, t: term, T: typ, maxidx: int, sorts: sort list}
    1.11 +  val crep_cterm: cterm ->
    1.12 +    {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
    1.13    val theory_of_cterm: cterm -> theory
    1.14    val sign_of_cterm: cterm -> theory    (*obsolete*)
    1.15    val term_of: cterm -> term
    1.16 @@ -95,7 +97,6 @@
    1.17    val combination: thm -> thm -> thm
    1.18    val equal_intr: thm -> thm -> thm
    1.19    val equal_elim: thm -> thm -> thm
    1.20 -  val implies_intr_hyps: thm -> thm
    1.21    val flexflex_rule: thm -> thm Seq.seq
    1.22    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    1.23    val trivial: cterm -> thm
    1.24 @@ -167,23 +168,28 @@
    1.25  
    1.26  fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) =
    1.27        map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts
    1.28 -  | dest_ctyp ct = [ct];
    1.29 +  | dest_ctyp cT = [cT];
    1.30  
    1.31  
    1.32  
    1.33  (** certified terms **)
    1.34  
    1.35 -(*certified terms with checked typ and maxidx of Vars/TVars*)
    1.36 +(*certified terms with checked typ, maxidx, and sorts*)
    1.37 +datatype cterm = Cterm of
    1.38 + {thy_ref: theory_ref,
    1.39 +  t: term,
    1.40 +  T: typ,
    1.41 +  maxidx: int,
    1.42 +  sorts: sort list};
    1.43  
    1.44 -datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int};
    1.45 -
    1.46 -fun rep_cterm (Cterm {thy_ref, t, T, maxidx}) =
    1.47 +fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
    1.48    let val thy =  Theory.deref thy_ref
    1.49 -  in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx} end;
    1.50 +  in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
    1.51  
    1.52 -fun crep_cterm (Cterm {thy_ref, t, T, maxidx}) =
    1.53 +fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
    1.54    let val thy = Theory.deref thy_ref in
    1.55 -    {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx}
    1.56 +   {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T},
    1.57 +    maxidx = maxidx, sorts = sorts}
    1.58    end;
    1.59  
    1.60  fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
    1.61 @@ -194,85 +200,87 @@
    1.62  fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T};
    1.63  
    1.64  fun cterm_of thy tm =
    1.65 -  let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm
    1.66 -  in  Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx}
    1.67 -  end;
    1.68 -
    1.69 +  let
    1.70 +    val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm;
    1.71 +    val sorts = Sorts.insert_term t [];
    1.72 +  in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
    1.73  
    1.74  exception CTERM of string;
    1.75  
    1.76  (*Destruct application in cterms*)
    1.77 -fun dest_comb (Cterm {thy_ref, T, maxidx, t = A $ B}) =
    1.78 +fun dest_comb (Cterm {thy_ref, T, maxidx, sorts, t = A $ B}) =
    1.79        let val typeA = fastype_of A;
    1.80            val typeB =
    1.81              case typeA of Type("fun",[S,T]) => S
    1.82 -                        | _ => error "Function type expected in dest_comb";
    1.83 +                        | _ => sys_error "Function type expected in dest_comb";
    1.84        in
    1.85 -      (Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA},
    1.86 -       Cterm {thy_ref=thy_ref, maxidx=maxidx, t=B, T=typeB})
    1.87 +      (Cterm {thy_ref=thy_ref, maxidx=maxidx, sorts=sorts, t=A, T=typeA},
    1.88 +       Cterm {thy_ref=thy_ref, maxidx=maxidx, sorts=sorts, t=B, T=typeB})
    1.89        end
    1.90    | dest_comb _ = raise CTERM "dest_comb";
    1.91  
    1.92  (*Destruct abstraction in cterms*)
    1.93 -fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
    1.94 +fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, sorts, t=Abs(x,ty,M)}) =
    1.95        let val (y,N) = variant_abs (if_none a x, ty, M)
    1.96 -      in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)},
    1.97 -          Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, t = N})
    1.98 +      in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, sorts = sorts, t = Free(y,ty)},
    1.99 +          Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, sorts = sorts, t = N})
   1.100        end
   1.101    | dest_abs _ _ = raise CTERM "dest_abs";
   1.102  
   1.103  (*Makes maxidx precise: it is often too big*)
   1.104 -fun adjust_maxidx (ct as Cterm {thy_ref, T, t, maxidx, ...}) =
   1.105 +fun adjust_maxidx (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   1.106    if maxidx = ~1 then ct
   1.107 -  else  Cterm {thy_ref = thy_ref, T = T, maxidx = maxidx_of_term t, t = t};
   1.108 +  else Cterm {thy_ref = thy_ref, t = t, T = T, maxidx = maxidx_of_term t, sorts = sorts};
   1.109  
   1.110  (*Form cterm out of a function and an argument*)
   1.111 -fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   1.112 -           (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) =
   1.113 -      if T = dty then
   1.114 -        Cterm{t = f $ x,
   1.115 -          thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty,
   1.116 -          maxidx=Int.max(maxidx1, maxidx2)}
   1.117 +fun capply
   1.118 +  (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1, sorts = sorts1})
   1.119 +  (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2, sorts = sorts2}) =
   1.120 +    if T = dty then
   1.121 +      Cterm{t = f $ x,
   1.122 +        thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty,
   1.123 +        maxidx=Int.max(maxidx1, maxidx2),
   1.124 +        sorts = Sorts.union sorts1 sorts2}
   1.125        else raise CTERM "capply: types don't agree"
   1.126    | capply _ _ = raise CTERM "capply: first arg is not a function"
   1.127  
   1.128 -fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1})
   1.129 -         (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) =
   1.130 -      Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2),
   1.131 -             T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   1.132 -      handle TERM _ => raise CTERM "cabs: first arg is not a variable";
   1.133 +fun cabs
   1.134 +  (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1, sorts = sorts1})
   1.135 +  (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2, sorts = sorts2}) =
   1.136 +    let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: first arg is not a variable" in
   1.137 +      Cterm {t = t, T = T1 --> T2, thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   1.138 +        maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2}
   1.139 +    end;
   1.140  
   1.141  (*Matching of cterms*)
   1.142  fun gen_cterm_match mtch
   1.143 -      (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...},
   1.144 -       Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, ...}) =
   1.145 +    (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, sorts = sorts1, ...},
   1.146 +     Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, sorts = sorts2, ...}) =
   1.147    let
   1.148      val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2);
   1.149      val tsig = Sign.tsig_of (Theory.deref thy_ref);
   1.150      val (Tinsts, tinsts) = mtch tsig (t1, t2);
   1.151      val maxidx = Int.max (maxidx1, maxidx2);
   1.152 +    val sorts = Sorts.union sorts1 sorts2;
   1.153      fun mk_cTinsts (ixn, (S, T)) =
   1.154        (Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)},
   1.155         Ctyp {thy_ref = thy_ref, T = T});
   1.156      fun mk_ctinsts (ixn, (T, t)) =
   1.157 -      let val T = Envir.typ_subst_TVars Tinsts T
   1.158 -      in
   1.159 -        (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
   1.160 -         Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t})
   1.161 +      let val T = Envir.typ_subst_TVars Tinsts T in
   1.162 +        (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T), sorts = sorts},
   1.163 +         Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t, sorts = sorts})
   1.164        end;
   1.165 -  in (map mk_cTinsts (Vartab.dest Tinsts),
   1.166 -    map mk_ctinsts (Vartab.dest tinsts))
   1.167 -  end;
   1.168 +  in (map mk_cTinsts (Vartab.dest Tinsts), map mk_ctinsts (Vartab.dest tinsts)) end;
   1.169  
   1.170  val cterm_match = gen_cterm_match Pattern.match;
   1.171  val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
   1.172  
   1.173  (*Incrementing indexes*)
   1.174 -fun cterm_incr_indexes i (ct as Cterm {thy_ref, maxidx, t, T}) =
   1.175 -  if i < 0 then raise CTERM "negative increment" else
   1.176 -  if i = 0 then ct else
   1.177 -    Cterm {thy_ref = thy_ref, maxidx = maxidx + i,
   1.178 -      t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};
   1.179 +fun cterm_incr_indexes i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   1.180 +  if i < 0 then raise CTERM "negative increment"
   1.181 +  else if i = 0 then ct
   1.182 +  else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t,
   1.183 +    T = Term.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
   1.184  
   1.185  
   1.186  
   1.187 @@ -307,12 +315,13 @@
   1.188   {thy_ref: theory_ref,         (*dynamic reference to theory*)
   1.189    der: bool * Pt.proof,        (*derivation*)
   1.190    maxidx: int,                 (*maximum index of any Var or TVar*)
   1.191 -  shyps: sort list,            (*sort hypotheses*)
   1.192 -  hyps: term list,             (*hypotheses*)
   1.193 +  shyps: sort list,            (*sort hypotheses as ordered list*)
   1.194 +  hyps: term list,             (*hypotheses as ordered list*)
   1.195    tpairs: (term * term) list,  (*flex-flex pairs*)
   1.196    prop: term};                 (*conclusion*)
   1.197  
   1.198  fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs);
   1.199 +val union_tpairs = gen_merge_lists (op = : (term * term) * (term * term) -> bool);
   1.200  
   1.201  fun attach_tpairs tpairs prop =
   1.202    Logic.list_implies (map Logic.mk_equals tpairs, prop);
   1.203 @@ -327,7 +336,7 @@
   1.204  fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   1.205    let
   1.206      val thy = Theory.deref thy_ref;
   1.207 -    fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max};
   1.208 +    fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
   1.209    in
   1.210     {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps,
   1.211      hyps = map (cterm ~1) hyps,
   1.212 @@ -345,6 +354,16 @@
   1.213  fun apply_attributes (x_th, atts) = Library.apply atts x_th;
   1.214  fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
   1.215  
   1.216 +
   1.217 +(* shyps and hyps *)
   1.218 +
   1.219 +val remove_hyps = OrdList.remove Term.term_ord;
   1.220 +val union_hyps = OrdList.union Term.term_ord;
   1.221 +val eq_set_hyps = OrdList.eq_set Term.term_ord;
   1.222 +
   1.223 +
   1.224 +(* eq_thm(s) *)
   1.225 +
   1.226  fun eq_thm (th1, th2) =
   1.227    let
   1.228      val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} =
   1.229 @@ -352,9 +371,9 @@
   1.230      val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} =
   1.231        rep_thm th2;
   1.232    in
   1.233 -    (subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso
   1.234 -    Sorts.eq_set_sort (shyps1, shyps2) andalso
   1.235 -    aconvs (hyps1, hyps2) andalso
   1.236 +    Context.joinable (thy1, thy2) andalso
   1.237 +    Sorts.eq_set (shyps1, shyps2) andalso
   1.238 +    eq_set_hyps (hyps1, hyps2) andalso
   1.239      aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
   1.240      prop1 aconv prop2
   1.241    end;
   1.242 @@ -366,13 +385,36 @@
   1.243  
   1.244  fun prop_of (Thm {prop, ...}) = prop;
   1.245  fun proof_of (Thm {der = (_, proof), ...}) = proof;
   1.246 +fun tpairs_of (Thm {tpairs, ...}) = tpairs;
   1.247  
   1.248 -(*merge theories of two theorems; raise exception if incompatible*)
   1.249 -fun merge_thm_thys
   1.250 -    (th1 as Thm {thy_ref = r1, ...}, th2 as Thm {thy_ref = r2, ...}) =
   1.251 +val concl_of = Logic.strip_imp_concl o prop_of;
   1.252 +val prems_of = Logic.strip_imp_prems o prop_of;
   1.253 +fun nprems_of th = Logic.count_prems (prop_of th, 0);
   1.254 +val no_prems = equal 0 o nprems_of;
   1.255 +
   1.256 +fun major_prem_of th =
   1.257 +  (case prems_of th of
   1.258 +    prem :: _ => Logic.strip_assums_concl prem
   1.259 +  | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
   1.260 +
   1.261 +(*the statement of any thm is a cterm*)
   1.262 +fun cprop_of (Thm {thy_ref, maxidx, shyps, prop, ...}) =
   1.263 +  Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
   1.264 +
   1.265 +
   1.266 +(* merge theories of cterms/thms; raise exception if incompatible *)
   1.267 +
   1.268 +fun merge_thys1
   1.269 +    (Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) =
   1.270 +  Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th]);
   1.271 +
   1.272 +fun merge_thys2
   1.273 +    (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) =
   1.274    Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   1.275  
   1.276 -(*transfer thm to super theory (non-destructive)*)
   1.277 +
   1.278 +(* explicit transfer thm to super theory *)
   1.279 +
   1.280  fun transfer thy' thm =
   1.281    let
   1.282      val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
   1.283 @@ -385,92 +427,21 @@
   1.284      else raise THM ("transfer: not a super theory", 0, [thm])
   1.285    end;
   1.286  
   1.287 -(*maps object-rule to tpairs*)
   1.288 -fun tpairs_of (Thm {tpairs, ...}) = tpairs;
   1.289 -
   1.290 -(*maps object-rule to premises*)
   1.291 -fun prems_of (Thm {prop, ...}) =
   1.292 -  Logic.strip_imp_prems prop;
   1.293 -
   1.294 -(*counts premises in a rule*)
   1.295 -fun nprems_of (Thm {prop, ...}) =
   1.296 -  Logic.count_prems (prop, 0);
   1.297 -
   1.298 -fun major_prem_of thm =
   1.299 -  (case prems_of thm of
   1.300 -    prem :: _ => Logic.strip_assums_concl prem
   1.301 -  | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));
   1.302 -
   1.303 -fun no_prems thm = nprems_of thm = 0;
   1.304 -
   1.305 -(*maps object-rule to conclusion*)
   1.306 -fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   1.307 -
   1.308 -(*the statement of any thm is a cterm*)
   1.309 -fun cprop_of (Thm {thy_ref, maxidx, prop, ...}) =
   1.310 -  Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop};
   1.311 -
   1.312  
   1.313  
   1.314  (** sort contexts of theorems **)
   1.315  
   1.316 -(* basic utils *)
   1.317 -
   1.318 -(*accumulate sorts suppressing duplicates; these are coded low levelly
   1.319 -  to improve efficiency a bit*)
   1.320 -
   1.321 -fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
   1.322 -  | add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss)
   1.323 -  | add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss)
   1.324 -and add_typs_sorts ([], Ss) = Ss
   1.325 -  | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
   1.326 -
   1.327 -fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
   1.328 -  | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
   1.329 -  | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
   1.330 -  | add_term_sorts (Bound _, Ss) = Ss
   1.331 -  | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
   1.332 -  | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));
   1.333 -
   1.334 -fun add_terms_sorts ([], Ss) = Ss
   1.335 -  | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
   1.336 -
   1.337 -fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs);
   1.338 -
   1.339 -fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
   1.340 -  Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd))
   1.341 -    (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol);
   1.342 +fun insert_env_sorts (env as Envir.Envir {iTs, asol, ...}) =
   1.343 +  Vartab.fold (fn (_, (_, t)) => Sorts.insert_term t) asol o
   1.344 +  Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) iTs;
   1.345  
   1.346 -fun add_insts_sorts ((iTs, is), Ss) =
   1.347 -  add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
   1.348 -
   1.349 -fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) =
   1.350 -  add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss));
   1.351 -
   1.352 -fun add_thms_shyps ([], Ss) = Ss
   1.353 -  | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
   1.354 -      add_thms_shyps (ths, Sorts.union_sort (shyps, Ss));
   1.355 -
   1.356 -
   1.357 -(*get 'dangling' sort constraints of a thm*)
   1.358 -fun extra_shyps (th as Thm {shyps, ...}) =
   1.359 -  Sorts.rems_sort (shyps, add_thm_sorts (th, []));
   1.360 +fun insert_thm_sorts (Thm {hyps, tpairs, prop, ...}) =
   1.361 +  fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs o
   1.362 +  Sorts.insert_terms hyps o Sorts.insert_term prop;
   1.363  
   1.364 -
   1.365 -(* fix_shyps *)
   1.366 -
   1.367 -val all_sorts_nonempty = is_some o Sign.universal_witness o Theory.deref;
   1.368 -
   1.369 -(*preserve sort contexts of rule premises and substituted types*)
   1.370 -fun fix_shyps thms Ts (thm as Thm {thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
   1.371 -  Thm
   1.372 -   {thy_ref = thy_ref,
   1.373 -    der = der,             (*no new derivation, as other rules call this*)
   1.374 -    maxidx = maxidx,
   1.375 -    shyps =
   1.376 -      if all_sorts_nonempty thy_ref then []
   1.377 -      else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
   1.378 -    hyps = hyps, tpairs = tpairs, prop = prop}
   1.379 +(*dangling sort constraints of a thm*)
   1.380 +fun extra_shyps (th as Thm {shyps, ...}) =
   1.381 +  Sorts.subtract (insert_thm_sorts th []) shyps;
   1.382  
   1.383  
   1.384  (* strip_shyps *)
   1.385 @@ -480,12 +451,12 @@
   1.386    | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   1.387        let
   1.388          val thy = Theory.deref thy_ref;
   1.389 -        val present_sorts = add_thm_sorts (thm, []);
   1.390 -        val extra_shyps = Sorts.rems_sort (shyps, present_sorts);
   1.391 +        val present_sorts = insert_thm_sorts thm [];
   1.392 +        val extra_shyps = Sorts.subtract present_sorts shyps;
   1.393          val witnessed_shyps = Sign.witness_sorts thy present_sorts extra_shyps;
   1.394        in
   1.395          Thm {thy_ref = thy_ref, der = der, maxidx = maxidx,
   1.396 -             shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps),
   1.397 +             shyps = Sorts.subtract (map #2 witnessed_shyps) shyps,
   1.398               hyps = hyps, tpairs = tpairs, prop = prop}
   1.399        end;
   1.400  
   1.401 @@ -498,15 +469,14 @@
   1.402    let
   1.403      fun get_ax thy =
   1.404        Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
   1.405 -      |> Option.map (fn t =>
   1.406 -          fix_shyps [] []
   1.407 -            (Thm {thy_ref = Theory.self_ref thy,
   1.408 -              der = Pt.infer_derivs' I (false, Pt.axm_proof name t),
   1.409 -              maxidx = maxidx_of_term t,
   1.410 -              shyps = [],
   1.411 -              hyps = [],
   1.412 -              tpairs = [],
   1.413 -              prop = t}));
   1.414 +      |> Option.map (fn prop =>
   1.415 +          Thm {thy_ref = Theory.self_ref thy,
   1.416 +            der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
   1.417 +            maxidx = maxidx_of_term prop,
   1.418 +            shyps = Sorts.insert_term prop [],
   1.419 +            hyps = [],
   1.420 +            tpairs = [],
   1.421 +            prop = prop});
   1.422    in
   1.423      (case get_first get_ax (theory :: Theory.ancestors_of theory) of
   1.424        SOME thm => thm
   1.425 @@ -559,26 +529,22 @@
   1.426  
   1.427  (*** Meta rules ***)
   1.428  
   1.429 -(** 'primitive' rules **)
   1.430 -
   1.431 -(*discharge all assumptions t from ts*)
   1.432 -val disch = gen_rem (op aconv);
   1.433 +(** primitive rules **)
   1.434  
   1.435 -(*The assumption rule A|-A in a theory*)
   1.436 -fun assume raw_ct : thm =
   1.437 -  let val ct as Cterm {thy_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
   1.438 -  in  if T<>propT then
   1.439 -        raise THM("assume: assumptions must have type prop", 0, [])
   1.440 -      else if maxidx <> ~1 then
   1.441 -        raise THM("assume: assumptions may not contain scheme variables",
   1.442 -                  maxidx, [])
   1.443 -      else Thm{thy_ref   = thy_ref,
   1.444 -               der    = Pt.infer_derivs' I (false, Pt.Hyp prop),
   1.445 -               maxidx = ~1,
   1.446 -               shyps  = add_term_sorts(prop,[]),
   1.447 -               hyps   = [prop],
   1.448 -               tpairs = [],
   1.449 -               prop   = prop}
   1.450 +(*The assumption rule A |- A in a theory*)
   1.451 +fun assume raw_ct =
   1.452 +  let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx raw_ct in
   1.453 +    if T <> propT then
   1.454 +      raise THM ("assume: assumptions must have type prop", 0, [])
   1.455 +    else if maxidx <> ~1 then
   1.456 +      raise THM ("assume: assumptions may not contain schematic variables", maxidx, [])
   1.457 +    else Thm {thy_ref = thy_ref,
   1.458 +      der = Pt.infer_derivs' I (false, Pt.Hyp prop),
   1.459 +      maxidx = ~1,
   1.460 +      shyps = sorts,
   1.461 +      hyps = [prop],
   1.462 +      tpairs = [],
   1.463 +      prop = prop}
   1.464    end;
   1.465  
   1.466  (*Implication introduction
   1.467 @@ -588,21 +554,19 @@
   1.468    -------
   1.469    A ==> B
   1.470  *)
   1.471 -fun implies_intr cA (thB as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm =
   1.472 -  let val Cterm {thy_ref=thy_refA, t=A, T, maxidx=maxidxA} = cA
   1.473 -  in  if T<>propT then
   1.474 -        raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   1.475 -      else
   1.476 -         Thm{thy_ref = Theory.merge_refs (thy_ref,thy_refA),
   1.477 -             der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   1.478 -             maxidx = Int.max(maxidxA, maxidx),
   1.479 -             shyps = add_term_sorts (A, shyps),
   1.480 -             hyps = disch(hyps,A),
   1.481 -             tpairs = tpairs,
   1.482 -             prop = implies$A$prop}
   1.483 -      handle TERM _ =>
   1.484 -        raise THM("implies_intr: incompatible theories", 0, [thB])
   1.485 -  end;
   1.486 +fun implies_intr
   1.487 +    (ct as Cterm {thy_ref = thy_refA, t = A, T, maxidx = maxidxA, sorts})
   1.488 +    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
   1.489 +  if T <> propT then
   1.490 +    raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   1.491 +  else
   1.492 +    Thm {thy_ref = merge_thys1 ct th,
   1.493 +      der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   1.494 +      maxidx = Int.max (maxidxA, maxidx),
   1.495 +      shyps = Sorts.union sorts shyps,
   1.496 +      hyps = remove_hyps A hyps,
   1.497 +      tpairs = tpairs,
   1.498 +      prop = implies $ A $ prop};
   1.499  
   1.500  
   1.501  (*Implication elimination
   1.502 @@ -610,48 +574,55 @@
   1.503    ------------
   1.504          B
   1.505  *)
   1.506 -fun implies_elim thAB thA : thm =
   1.507 -    let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, tpairs=tpairsA, prop=propA, ...} = thA
   1.508 -        and Thm{der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB;
   1.509 -        fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   1.510 -    in  case prop of
   1.511 -            imp$A$B =>
   1.512 -                if imp=implies andalso  A aconv propA
   1.513 -                then
   1.514 -                  Thm{thy_ref= merge_thm_thys (thAB, thA),
   1.515 -                      der = Pt.infer_derivs (curry Pt.%%) der derA,
   1.516 -                      maxidx = Int.max(maxA,maxidx),
   1.517 -                      shyps = Sorts.union_sort (shypsA, shyps),
   1.518 -                      hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   1.519 -                      tpairs = tpairsA @ tpairs,
   1.520 -                      prop = B}
   1.521 -                else err("major premise")
   1.522 -          | _ => err("major premise")
   1.523 -    end;
   1.524 +fun implies_elim thAB thA =
   1.525 +  let
   1.526 +    val Thm {maxidx = maxA, der = derA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
   1.527 +      prop = propA, ...} = thA
   1.528 +    and Thm {der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB;
   1.529 +    fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   1.530 +  in
   1.531 +    case prop of
   1.532 +      imp $ A $ B =>
   1.533 +        if imp = Term.implies andalso A aconv propA then
   1.534 +          Thm {thy_ref= merge_thys2 thAB thA,
   1.535 +            der = Pt.infer_derivs (curry Pt.%%) der derA,
   1.536 +            maxidx = Int.max (maxA, maxidx),
   1.537 +            shyps = Sorts.union shypsA shyps,
   1.538 +            hyps = union_hyps hypsA hyps,
   1.539 +            tpairs = union_tpairs tpairsA tpairs,
   1.540 +            prop = B}
   1.541 +        else err ()
   1.542 +    | _ => err ()
   1.543 +  end;
   1.544  
   1.545  (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
   1.546 +   [x]
   1.547 +    :
   1.548      A
   1.549    -----
   1.550    !!x.A
   1.551  *)
   1.552 -fun forall_intr cx (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) =
   1.553 -  let val x = term_of cx;
   1.554 -      fun result a T = fix_shyps [th] []
   1.555 -        (Thm{thy_ref = thy_ref,
   1.556 -             der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
   1.557 -             maxidx = maxidx,
   1.558 -             shyps = [],
   1.559 -             hyps = hyps,
   1.560 -             tpairs = tpairs,
   1.561 -             prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   1.562 -      fun check_occs x ts =
   1.563 -        if exists (apl(x, Logic.occs)) ts
   1.564 -        then raise THM("forall_intr: variable free in assumptions", 0, [th])
   1.565 -        else ()
   1.566 -  in  case x of
   1.567 -        Free(a,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result a T)
   1.568 -      | Var((a,_),T) => (check_occs x (terms_of_tpairs tpairs); result a T)
   1.569 -      | _ => raise THM("forall_intr: not a variable", 0, [th])
   1.570 +fun forall_intr
   1.571 +    (ct as Cterm {t = x, T, sorts, ...})
   1.572 +    (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   1.573 +  let
   1.574 +    fun result a =
   1.575 +      Thm {thy_ref = merge_thys1 ct th,
   1.576 +        der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
   1.577 +        maxidx = maxidx,
   1.578 +        shyps = Sorts.union sorts shyps,
   1.579 +        hyps = hyps,
   1.580 +        tpairs = tpairs,
   1.581 +        prop = all T $ Abs (a, T, abstract_over (x, prop))};
   1.582 +    fun check_occs x ts =
   1.583 +      if exists (apl (x, Logic.occs)) ts then
   1.584 +        raise THM("forall_intr: variable free in assumptions", 0, [th])
   1.585 +      else ();
   1.586 +  in
   1.587 +    case x of
   1.588 +      Free (a, _) => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result a)
   1.589 +    | Var ((a, _), _) => (check_occs x (terms_of_tpairs tpairs); result a)
   1.590 +    | _ => raise THM ("forall_intr: not a variable", 0, [th])
   1.591    end;
   1.592  
   1.593  (*Forall elimination
   1.594 @@ -659,224 +630,227 @@
   1.595    ------
   1.596    A[t/x]
   1.597  *)
   1.598 -fun forall_elim ct (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) : thm =
   1.599 -  let val Cterm {thy_ref=thy_reft, t, T, maxidx=maxt} = ct
   1.600 -  in  case prop of
   1.601 -        Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   1.602 -          if T<>qary then
   1.603 -              raise THM("forall_elim: type mismatch", 0, [th])
   1.604 -          else fix_shyps [th] []
   1.605 -                    (Thm{thy_ref= Theory.merge_refs(thy_ref,thy_reft),
   1.606 -                         der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
   1.607 -                         maxidx = Int.max(maxidx, maxt),
   1.608 -                         shyps = [],
   1.609 -                         hyps = hyps,
   1.610 -                         tpairs = tpairs,
   1.611 -                         prop = betapply(A,t)})
   1.612 -      | _ => raise THM("forall_elim: not quantified", 0, [th])
   1.613 -  end
   1.614 -  handle TERM _ =>
   1.615 -         raise THM("forall_elim: incompatible theories", 0, [th]);
   1.616 +fun forall_elim
   1.617 +    (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
   1.618 +    (th as Thm {der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   1.619 +  (case prop of
   1.620 +    Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
   1.621 +      if T <> qary then
   1.622 +        raise THM ("forall_elim: type mismatch", 0, [th])
   1.623 +      else
   1.624 +        Thm {thy_ref = merge_thys1 ct th,
   1.625 +          der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
   1.626 +          maxidx = Int.max (maxidx, maxt),
   1.627 +          shyps = Sorts.union sorts shyps,
   1.628 +          hyps = hyps,
   1.629 +          tpairs = tpairs,
   1.630 +          prop = Term.betapply (A, t)}
   1.631 +  | _ => raise THM ("forall_elim: not quantified", 0, [th]));
   1.632  
   1.633  
   1.634  (* Equality *)
   1.635  
   1.636 -(*The reflexivity rule: maps  t   to the theorem   t==t   *)
   1.637 -fun reflexive ct =
   1.638 -  let val Cterm {thy_ref, t, T, maxidx} = ct
   1.639 -  in Thm{thy_ref= thy_ref,
   1.640 -         der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.641 -         shyps = add_term_sorts (t, []),
   1.642 -         hyps = [],
   1.643 -         maxidx = maxidx,
   1.644 -         tpairs = [],
   1.645 -         prop = Logic.mk_equals(t,t)}
   1.646 -  end;
   1.647 +(*Reflexivity
   1.648 +  t == t
   1.649 +*)
   1.650 +fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   1.651 +  Thm {thy_ref= thy_ref,
   1.652 +    der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.653 +    maxidx = maxidx,
   1.654 +    shyps = sorts,
   1.655 +    hyps = [],
   1.656 +    tpairs = [],
   1.657 +    prop = Logic.mk_equals (t, t)};
   1.658  
   1.659 -(*The symmetry rule
   1.660 -  t==u
   1.661 -  ----
   1.662 -  u==t
   1.663 +(*Symmetry
   1.664 +  t == u
   1.665 +  ------
   1.666 +  u == t
   1.667  *)
   1.668 -fun symmetric (th as Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   1.669 -  case prop of
   1.670 -      (eq as Const("==", Type (_, [T, _]))) $ t $ u =>
   1.671 -        (*no fix_shyps*)
   1.672 -          Thm{thy_ref = thy_ref,
   1.673 -              der = Pt.infer_derivs' Pt.symmetric der,
   1.674 -              maxidx = maxidx,
   1.675 -              shyps = shyps,
   1.676 -              hyps = hyps,
   1.677 -              tpairs = tpairs,
   1.678 -              prop = eq$u$t}
   1.679 -    | _ => raise THM("symmetric", 0, [th]);
   1.680 +fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   1.681 +  (case prop of
   1.682 +    (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
   1.683 +      Thm {thy_ref = thy_ref,
   1.684 +        der = Pt.infer_derivs' Pt.symmetric der,
   1.685 +        maxidx = maxidx,
   1.686 +        shyps = shyps,
   1.687 +        hyps = hyps,
   1.688 +        tpairs = tpairs,
   1.689 +        prop = eq $ u $ t}
   1.690 +    | _ => raise THM ("symmetric", 0, [th]));
   1.691  
   1.692 -(*The transitive rule
   1.693 -  t1==u    u==t2
   1.694 -  --------------
   1.695 -      t1==t2
   1.696 +(*Transitivity
   1.697 +  t1 == u    u == t2
   1.698 +  ------------------
   1.699 +       t1 == t2
   1.700  *)
   1.701  fun transitive th1 th2 =
   1.702 -  let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1
   1.703 -      and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2;
   1.704 -      fun err msg = raise THM("transitive: "^msg, 0, [th1,th2])
   1.705 -  in case (prop1,prop2) of
   1.706 -       ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   1.707 -          if not (u aconv u') then err"middle term"
   1.708 -          else
   1.709 -                 Thm{thy_ref= merge_thm_thys (th1, th2),
   1.710 -                     der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   1.711 -                     maxidx = Int.max(max1,max2),
   1.712 -                     shyps = Sorts.union_sort (shyps1, shyps2),
   1.713 -                     hyps = union_term(hyps1,hyps2),
   1.714 -                     tpairs = tpairs1 @ tpairs2,
   1.715 -                     prop = eq$t1$t2}
   1.716 -     | _ =>  err"premises"
   1.717 +  let
   1.718 +    val Thm {der = der1, maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
   1.719 +      prop = prop1, ...} = th1
   1.720 +    and Thm {der = der2, maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
   1.721 +      prop = prop2, ...} = th2;
   1.722 +    fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   1.723 +  in
   1.724 +    case (prop1, prop2) of
   1.725 +      ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
   1.726 +        if not (u aconv u') then err "middle term"
   1.727 +        else
   1.728 +          Thm {thy_ref= merge_thys2 th1 th2,
   1.729 +            der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   1.730 +            maxidx = Int.max (max1, max2),
   1.731 +            shyps = Sorts.union shyps1 shyps2,
   1.732 +            hyps = union_hyps hyps1 hyps2,
   1.733 +            tpairs = union_tpairs tpairs1 tpairs2,
   1.734 +            prop = eq $ t1 $ t2}
   1.735 +     | _ =>  err "premises"
   1.736    end;
   1.737  
   1.738 -(*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x]
   1.739 -  Fully beta-reduces the term if full=true
   1.740 +(*Beta-conversion
   1.741 +  (%x.t)(u) == t[u/x]
   1.742 +  fully beta-reduces the term if full = true
   1.743  *)
   1.744 -fun beta_conversion full ct =
   1.745 -  let val Cterm {thy_ref, t, T, maxidx} = ct
   1.746 -  in Thm
   1.747 -    {thy_ref = thy_ref,
   1.748 -     der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.749 -     maxidx = maxidx,
   1.750 -     shyps = add_term_sorts (t, []),
   1.751 -     hyps = [],
   1.752 -     tpairs = [],
   1.753 -     prop = Logic.mk_equals (t, if full then Envir.beta_norm t
   1.754 -       else case t of
   1.755 -          Abs(_, _, bodt) $ u => subst_bound (u, bodt)
   1.756 -        | _ => raise THM ("beta_conversion: not a redex", 0, []))}
   1.757 +fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) =
   1.758 +  let val t' =
   1.759 +    if full then Envir.beta_norm t
   1.760 +    else
   1.761 +      (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
   1.762 +      | _ => raise THM ("beta_conversion: not a redex", 0, []));
   1.763 +  in
   1.764 +    Thm {thy_ref = thy_ref,
   1.765 +      der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.766 +      maxidx = maxidx,
   1.767 +      shyps = sorts,
   1.768 +      hyps = [],
   1.769 +      tpairs = [],
   1.770 +      prop = Logic.mk_equals (t, t')}
   1.771    end;
   1.772  
   1.773 -fun eta_conversion ct =
   1.774 -  let val Cterm {thy_ref, t, T, maxidx} = ct
   1.775 -  in Thm
   1.776 -    {thy_ref = thy_ref,
   1.777 -     der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.778 -     maxidx = maxidx,
   1.779 -     shyps = add_term_sorts (t, []),
   1.780 -     hyps = [],
   1.781 -     tpairs = [],
   1.782 -     prop = Logic.mk_equals (t, Pattern.eta_contract t)}
   1.783 -  end;
   1.784 +fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   1.785 +  Thm {thy_ref = thy_ref,
   1.786 +    der = Pt.infer_derivs' I (false, Pt.reflexive),
   1.787 +    maxidx = maxidx,
   1.788 +    shyps = sorts,
   1.789 +    hyps = [],
   1.790 +    tpairs = [],
   1.791 +    prop = Logic.mk_equals (t, Pattern.eta_contract t)};
   1.792  
   1.793  (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   1.794    The bound variable will be named "a" (since x will be something like x320)
   1.795 -     t == u
   1.796 -  ------------
   1.797 -  %x.t == %x.u
   1.798 +      t == u
   1.799 +  --------------
   1.800 +  %x. t == %x. u
   1.801  *)
   1.802 -fun abstract_rule a cx (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) =
   1.803 -  let val x = term_of cx;
   1.804 -      val (t,u) = Logic.dest_equals prop
   1.805 -            handle TERM _ =>
   1.806 -                raise THM("abstract_rule: premise not an equality", 0, [th])
   1.807 -      fun result T =
   1.808 -           Thm{thy_ref = thy_ref,
   1.809 -               der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
   1.810 -               maxidx = maxidx,
   1.811 -               shyps = add_typ_sorts (T, shyps),
   1.812 -               hyps = hyps,
   1.813 -               tpairs = tpairs,
   1.814 -               prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   1.815 -                                      Abs(a, T, abstract_over (x,u)))}
   1.816 -      fun check_occs x ts =
   1.817 -         if exists (apl(x, Logic.occs)) ts
   1.818 -         then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   1.819 -         else ()
   1.820 -  in  case x of
   1.821 -        Free(_,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result T)
   1.822 -      | Var(_,T) => (check_occs x (terms_of_tpairs tpairs); result T)
   1.823 -      | _ => raise THM("abstract_rule: not a variable", 0, [th])
   1.824 +fun abstract_rule a
   1.825 +    (Cterm {t = x, T, sorts, ...})
   1.826 +    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
   1.827 +  let
   1.828 +    val (t, u) = Logic.dest_equals prop
   1.829 +      handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
   1.830 +    val result =
   1.831 +      Thm {thy_ref = thy_ref,
   1.832 +        der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
   1.833 +        maxidx = maxidx,
   1.834 +        shyps = Sorts.union sorts shyps,
   1.835 +        hyps = hyps,
   1.836 +        tpairs = tpairs,
   1.837 +        prop = Logic.mk_equals
   1.838 +          (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))};
   1.839 +    fun check_occs x ts =
   1.840 +      if exists (apl (x, Logic.occs)) ts then
   1.841 +        raise THM ("abstract_rule: variable free in assumptions", 0, [th])
   1.842 +      else ();
   1.843 +  in
   1.844 +    case x of
   1.845 +      Free _ => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result)
   1.846 +    | Var _ => (check_occs x (terms_of_tpairs tpairs); result)
   1.847 +    | _ => raise THM ("abstract_rule: not a variable", 0, [th])
   1.848    end;
   1.849  
   1.850  (*The combination rule
   1.851    f == g  t == u
   1.852    --------------
   1.853 -   f(t) == g(u)
   1.854 +    f t == g u
   1.855  *)
   1.856  fun combination th1 th2 =
   1.857 -  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
   1.858 -              tpairs=tpairs1, prop=prop1,...} = th1
   1.859 -      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
   1.860 -              tpairs=tpairs2, prop=prop2,...} = th2
   1.861 -      fun chktypes fT tT =
   1.862 -            (case fT of
   1.863 -                Type("fun",[T1,T2]) =>
   1.864 -                    if T1 <> tT then
   1.865 -                         raise THM("combination: types", 0, [th1,th2])
   1.866 -                    else ()
   1.867 -                | _ => raise THM("combination: not function type", 0,
   1.868 -                                 [th1,th2]))
   1.869 -  in case (prop1,prop2)  of
   1.870 -       (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   1.871 -        Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   1.872 -          (chktypes fT tT;
   1.873 -                        (*no fix_shyps*)
   1.874 -                        Thm{thy_ref = merge_thm_thys(th1,th2),
   1.875 -                            der = Pt.infer_derivs
   1.876 -                              (Pt.combination f g t u fT) der1 der2,
   1.877 -                            maxidx = Int.max(max1,max2),
   1.878 -                            shyps = Sorts.union_sort(shyps1,shyps2),
   1.879 -                            hyps = union_term(hyps1,hyps2),
   1.880 -                            tpairs = tpairs1 @ tpairs2,
   1.881 -                            prop = Logic.mk_equals(f$t, g$u)})
   1.882 -     | _ =>  raise THM("combination: premises", 0, [th1,th2])
   1.883 +  let
   1.884 +    val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   1.885 +      prop = prop1, ...} = th1
   1.886 +    and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   1.887 +      prop = prop2, ...} = th2;
   1.888 +    fun chktypes fT tT =
   1.889 +      (case fT of
   1.890 +        Type ("fun", [T1, T2]) =>
   1.891 +          if T1 <> tT then
   1.892 +            raise THM ("combination: types", 0, [th1, th2])
   1.893 +          else ()
   1.894 +      | _ => raise THM ("combination: not function type", 0, [th1, th2]));
   1.895 +  in
   1.896 +    case (prop1, prop2) of
   1.897 +      (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   1.898 +       Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   1.899 +        (chktypes fT tT;
   1.900 +          Thm {thy_ref = merge_thys2 th1 th2,
   1.901 +            der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2,
   1.902 +            maxidx = Int.max (max1, max2),
   1.903 +            shyps = Sorts.union shyps1 shyps2,
   1.904 +            hyps = union_hyps hyps1 hyps2,
   1.905 +            tpairs = union_tpairs tpairs1 tpairs2,
   1.906 +            prop = Logic.mk_equals (f $ t, g $ u)})
   1.907 +     | _ => raise THM ("combination: premises", 0, [th1, th2])
   1.908    end;
   1.909  
   1.910 -
   1.911 -(* Equality introduction
   1.912 +(*Equality introduction
   1.913    A ==> B  B ==> A
   1.914    ----------------
   1.915         A == B
   1.916  *)
   1.917  fun equal_intr th1 th2 =
   1.918 -  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
   1.919 -              tpairs=tpairs1, prop=prop1,...} = th1
   1.920 -      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
   1.921 -              tpairs=tpairs2, prop=prop2,...} = th2;
   1.922 -      fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   1.923 -  in case (prop1,prop2) of
   1.924 -       (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   1.925 -          if A aconv A' andalso B aconv B'
   1.926 -          then
   1.927 -            (*no fix_shyps*)
   1.928 -              Thm{thy_ref = merge_thm_thys(th1,th2),
   1.929 -                  der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
   1.930 -                  maxidx = Int.max(max1,max2),
   1.931 -                  shyps = Sorts.union_sort(shyps1,shyps2),
   1.932 -                  hyps = union_term(hyps1,hyps2),
   1.933 -                  tpairs = tpairs1 @ tpairs2,
   1.934 -                  prop = Logic.mk_equals(A,B)}
   1.935 -          else err"not equal"
   1.936 -     | _ =>  err"premises"
   1.937 +  let
   1.938 +    val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   1.939 +      prop = prop1, ...} = th1
   1.940 +    and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   1.941 +      prop = prop2, ...} = th2;
   1.942 +    fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   1.943 +  in
   1.944 +    case (prop1, prop2) of
   1.945 +      (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
   1.946 +        if A aconv A' andalso B aconv B' then
   1.947 +          Thm {thy_ref = merge_thys2 th1 th2,
   1.948 +            der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
   1.949 +            maxidx = Int.max (max1, max2),
   1.950 +            shyps = Sorts.union shyps1 shyps2,
   1.951 +            hyps = union_hyps hyps1 hyps2,
   1.952 +            tpairs = union_tpairs tpairs1 tpairs2,
   1.953 +            prop = Logic.mk_equals (A, B)}
   1.954 +        else err "not equal"
   1.955 +    | _ =>  err "premises"
   1.956    end;
   1.957  
   1.958 -
   1.959  (*The equal propositions rule
   1.960    A == B  A
   1.961    ---------
   1.962        B
   1.963  *)
   1.964  fun equal_elim th1 th2 =
   1.965 -  let val Thm{der=der1, maxidx=max1, hyps=hyps1, tpairs=tpairs1, prop=prop1,...} = th1
   1.966 -      and Thm{der=der2, maxidx=max2, hyps=hyps2, tpairs=tpairs2, prop=prop2,...} = th2;
   1.967 -      fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   1.968 -  in  case prop1  of
   1.969 -       Const("==",_) $ A $ B =>
   1.970 -          if not (prop2 aconv A) then err"not equal"  else
   1.971 -            fix_shyps [th1, th2] []
   1.972 -              (Thm{thy_ref= merge_thm_thys(th1,th2),
   1.973 -                   der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
   1.974 -                   maxidx = Int.max(max1,max2),
   1.975 -                   shyps = [],
   1.976 -                   hyps = union_term(hyps1,hyps2),
   1.977 -                   tpairs = tpairs1 @ tpairs2,
   1.978 -                   prop = B})
   1.979 +  let
   1.980 +    val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1,
   1.981 +      tpairs = tpairs1, prop = prop1, ...} = th1
   1.982 +    and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2,
   1.983 +      tpairs = tpairs2, prop = prop2, ...} = th2;
   1.984 +    fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
   1.985 +  in
   1.986 +    case prop1 of
   1.987 +      Const ("==", _) $ A $ B =>
   1.988 +        if prop2 aconv A then
   1.989 +          Thm {thy_ref = merge_thys2 th1 th2,
   1.990 +            der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
   1.991 +            maxidx = Int.max (max1, max2),
   1.992 +            shyps = Sorts.union shyps1 shyps2,
   1.993 +            hyps = union_hyps hyps1 hyps2,
   1.994 +            tpairs = union_tpairs tpairs1 tpairs2,
   1.995 +            prop = B}
   1.996 +        else err "not equal"
   1.997       | _ =>  err"major premise"
   1.998    end;
   1.999  
  1.1000 @@ -884,84 +858,71 @@
  1.1001  
  1.1002  (**** Derived rules ****)
  1.1003  
  1.1004 -(*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
  1.1005 -  Repeated hypotheses are discharged only once;  fold cannot do this*)
  1.1006 -fun implies_intr_hyps (Thm{thy_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) =
  1.1007 -      implies_intr_hyps (*no fix_shyps*)
  1.1008 -            (Thm{thy_ref = thy_ref,
  1.1009 -                 der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
  1.1010 -                 maxidx = maxidx,
  1.1011 -                 shyps = shyps,
  1.1012 -                 hyps = disch(As,A),
  1.1013 -                 tpairs = tpairs,
  1.1014 -                 prop = implies$A$prop})
  1.1015 -  | implies_intr_hyps th = th;
  1.1016 -
  1.1017 -(*Smash" unifies the list of term pairs leaving no flex-flex pairs.
  1.1018 +(*Smash unifies the list of term pairs leaving no flex-flex pairs.
  1.1019    Instantiates the theorem and deletes trivial tpairs.
  1.1020    Resulting sequence may contain multiple elements if the tpairs are
  1.1021      not all flex-flex. *)
  1.1022 -fun flexflex_rule (th as Thm{thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
  1.1023 -  let fun newthm env =
  1.1024 -          if Envir.is_empty env then th
  1.1025 -          else
  1.1026 -          let val ntpairs = map (pairself (Envir.norm_term env)) tpairs;
  1.1027 -              val newprop = Envir.norm_term env prop;
  1.1028 -                (*Remove trivial tpairs, of the form t=t*)
  1.1029 -              val distpairs = List.filter (not o op aconv) ntpairs
  1.1030 -          in  fix_shyps [th] (env_codT env)
  1.1031 -                (Thm{thy_ref = thy_ref,
  1.1032 -                     der = Pt.infer_derivs' (Pt.norm_proof' env) der,
  1.1033 -                     maxidx = maxidx_of_terms (newprop ::
  1.1034 -                       terms_of_tpairs distpairs),
  1.1035 -                     shyps = [],
  1.1036 -                     hyps = hyps,
  1.1037 -                     tpairs = distpairs,
  1.1038 -                     prop = newprop})
  1.1039 -          end;
  1.1040 -  in Seq.map newthm
  1.1041 -            (Unify.smash_unifiers(Theory.deref thy_ref, Envir.empty maxidx, tpairs))
  1.1042 -  end;
  1.1043 +fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  1.1044 +  Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs)
  1.1045 +  |> Seq.map (fn env =>
  1.1046 +      if Envir.is_empty env then th
  1.1047 +      else
  1.1048 +        let
  1.1049 +          val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
  1.1050 +            (*remove trivial tpairs, of the form t==t*)
  1.1051 +            |> List.filter (not o op aconv);
  1.1052 +          val prop' = Envir.norm_term env prop;
  1.1053 +        in
  1.1054 +          Thm {thy_ref = thy_ref,
  1.1055 +            der = Pt.infer_derivs' (Pt.norm_proof' env) der,
  1.1056 +            maxidx = maxidx_of_terms (prop' :: terms_of_tpairs tpairs'),
  1.1057 +            shyps = insert_env_sorts env shyps,
  1.1058 +            hyps = hyps,
  1.1059 +            tpairs = tpairs',
  1.1060 +            prop = prop'}
  1.1061 +        end);
  1.1062 +
  1.1063  
  1.1064  (*Instantiation of Vars
  1.1065 -           A
  1.1066 -  -------------------
  1.1067 -  A[t1/v1,....,tn/vn]
  1.1068 +            A
  1.1069 +  ---------------------
  1.1070 +  A[t1/v1, ...., tn/vn]
  1.1071  *)
  1.1072  
  1.1073  local
  1.1074  
  1.1075  (*Check that all the terms are Vars and are distinct*)
  1.1076 -fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
  1.1077 +fun instl_ok ts = forall is_Var ts andalso null (findrep ts);
  1.1078  
  1.1079  fun pretty_typing thy t T =
  1.1080    Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
  1.1081  
  1.1082  (*For instantiate: process pair of cterms, merge theories*)
  1.1083 -fun add_ctpair ((ct,cu), (thy_ref,tpairs)) =
  1.1084 +fun add_ctpair ((ct, cu), (thy_ref, tpairs)) =
  1.1085    let
  1.1086 -    val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct
  1.1087 -    and Cterm {thy_ref=thy_refu, t=u, T= U, ...} = cu;
  1.1088 +    val Cterm {thy_ref = thy_reft, t = t, T = T, ...} = ct
  1.1089 +    and Cterm {thy_ref = thy_refu, t = u, T = U, ...} = cu;
  1.1090      val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu));
  1.1091      val thy_merged = Theory.deref thy_ref_merged;
  1.1092    in
  1.1093 -    if T=U then (thy_ref_merged, (t,u)::tpairs)
  1.1094 -    else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict",
  1.1095 +    if T = U then (thy_ref_merged, (t, u) :: tpairs)
  1.1096 +    else raise TYPE (Pretty.string_of (Pretty.block
  1.1097 +     [Pretty.str "instantiate: type conflict",
  1.1098        Pretty.fbrk, pretty_typing thy_merged t T,
  1.1099        Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u])
  1.1100    end;
  1.1101  
  1.1102 -fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT},
  1.1103 -      Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) =
  1.1104 +fun add_ctyp
  1.1105 +  ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT},
  1.1106 +    Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) =
  1.1107        let
  1.1108          val thy_ref_merged = Theory.merge_refs
  1.1109            (thy_ref, Theory.merge_refs (thy_refT, thy_refU));
  1.1110 -        val thy_merged = Theory.deref thy_ref_merged
  1.1111 +        val thy_merged = Theory.deref thy_ref_merged;
  1.1112        in
  1.1113          if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then
  1.1114            (thy_ref_merged, (T, U) :: vTs)
  1.1115 -        else raise TYPE ("Type not of sort " ^
  1.1116 -          Sign.string_of_sort thy_merged S, [U], [])
  1.1117 +        else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy_merged S, [U], [])
  1.1118        end
  1.1119    | add_ctyp ((Ctyp {T, thy_ref}, _), _) =
  1.1120        raise TYPE (Pretty.string_of (Pretty.block
  1.1121 @@ -970,105 +931,103 @@
  1.1122  
  1.1123  in
  1.1124  
  1.1125 -(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
  1.1126 +(*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
  1.1127    Instantiates distinct Vars by terms of same type.
  1.1128 -  No longer normalizes the new theorem! *)
  1.1129 +  Does NOT normalize the resulting theorem!*)
  1.1130  fun instantiate ([], []) th = th
  1.1131 -  | instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
  1.1132 -  let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs;
  1.1133 -      val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs;
  1.1134 -      fun subst t =
  1.1135 -        subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
  1.1136 -      val newprop = subst prop;
  1.1137 -      val newdpairs = map (pairself subst) dpairs;
  1.1138 -      val newth =
  1.1139 -            (Thm{thy_ref = newthy_ref,
  1.1140 -                 der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
  1.1141 -                 maxidx = maxidx_of_terms (newprop ::
  1.1142 -                   terms_of_tpairs newdpairs),
  1.1143 -                 shyps = add_insts_sorts ((vTs, tpairs), shyps),
  1.1144 -                 hyps = hyps,
  1.1145 -                 tpairs = newdpairs,
  1.1146 -                 prop = newprop})
  1.1147 -  in  if not(instl_ok(map #1 tpairs))
  1.1148 -      then raise THM("instantiate: variables not distinct", 0, [th])
  1.1149 -      else if not(null(findrep(map #1 vTs)))
  1.1150 -      then raise THM("instantiate: type variables not distinct", 0, [th])
  1.1151 -      else newth
  1.1152 +  | instantiate (vcTs, ctpairs) th =
  1.1153 +  let
  1.1154 +    val Thm {thy_ref, der, maxidx, hyps, shyps, tpairs = dpairs, prop} = th;
  1.1155 +    val (newthy_ref, tpairs) = foldr add_ctpair (thy_ref, []) ctpairs;
  1.1156 +    val (newthy_ref, vTs) = foldr add_ctyp (newthy_ref, []) vcTs;
  1.1157 +    fun subst t = subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
  1.1158 +    val newprop = subst prop;
  1.1159 +    val newdpairs = map (pairself subst) dpairs;
  1.1160 +    val newth =
  1.1161 +      Thm {thy_ref = newthy_ref,
  1.1162 +        der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
  1.1163 +        maxidx = maxidx_of_terms (newprop :: terms_of_tpairs newdpairs),
  1.1164 +        shyps = shyps
  1.1165 +          |> fold (Sorts.insert_typ o #2) vTs
  1.1166 +          |> fold (Sorts.insert_term o #2) tpairs,
  1.1167 +        hyps = hyps,
  1.1168 +        tpairs = newdpairs,
  1.1169 +        prop = newprop};
  1.1170 +  in
  1.1171 +    if not (instl_ok (map #1 tpairs)) then
  1.1172 +      raise THM ("instantiate: variables not distinct", 0, [th])
  1.1173 +    else if not (null (findrep (map #1 vTs))) then
  1.1174 +      raise THM ("instantiate: type variables not distinct", 0, [th])
  1.1175 +    else newth
  1.1176    end
  1.1177 -  handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th])
  1.1178 -       | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  1.1179 +  handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  1.1180  
  1.1181  end;
  1.1182  
  1.1183  
  1.1184 -(*The trivial implication A==>A, justified by assume and forall rules.
  1.1185 -  A can contain Vars, not so for assume!   *)
  1.1186 -fun trivial ct : thm =
  1.1187 -  let val Cterm {thy_ref, t=A, T, maxidx} = ct
  1.1188 -  in  if T<>propT then
  1.1189 -            raise THM("trivial: the term must have type prop", 0, [])
  1.1190 -      else fix_shyps [] []
  1.1191 -        (Thm{thy_ref = thy_ref,
  1.1192 -             der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
  1.1193 -             maxidx = maxidx,
  1.1194 -             shyps = [],
  1.1195 -             hyps = [],
  1.1196 -             tpairs = [],
  1.1197 -             prop = implies$A$A})
  1.1198 -  end;
  1.1199 +(*The trivial implication A ==> A, justified by assume and forall rules.
  1.1200 +  A can contain Vars, not so for assume!*)
  1.1201 +fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) =
  1.1202 +  if T <> propT then
  1.1203 +    raise THM ("trivial: the term must have type prop", 0, [])
  1.1204 +  else
  1.1205 +    Thm {thy_ref = thy_ref,
  1.1206 +      der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
  1.1207 +      maxidx = maxidx,
  1.1208 +      shyps = sorts,
  1.1209 +      hyps = [],
  1.1210 +      tpairs = [],
  1.1211 +      prop = implies $ A $ A};
  1.1212  
  1.1213  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
  1.1214  fun class_triv thy c =
  1.1215 -  let val Cterm {thy_ref, t, maxidx, ...} =
  1.1216 +  let val Cterm {thy_ref, t, maxidx, sorts, ...} =
  1.1217      cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
  1.1218        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
  1.1219    in
  1.1220 -    fix_shyps [] []
  1.1221 -      (Thm {thy_ref = thy_ref,
  1.1222 -            der = Pt.infer_derivs' I
  1.1223 -              (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
  1.1224 -            maxidx = maxidx,
  1.1225 -            shyps = [],
  1.1226 -            hyps = [],
  1.1227 -            tpairs = [],
  1.1228 -            prop = t})
  1.1229 +    Thm {thy_ref = thy_ref,
  1.1230 +      der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
  1.1231 +      maxidx = maxidx,
  1.1232 +      shyps = sorts,
  1.1233 +      hyps = [],
  1.1234 +      tpairs = [],
  1.1235 +      prop = t}
  1.1236    end;
  1.1237  
  1.1238  
  1.1239  (* Replace all TFrees not fixed or in the hyps by new TVars *)
  1.1240 -fun varifyT' fixed (Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  1.1241 +fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  1.1242    let
  1.1243      val tfrees = foldr add_term_tfrees fixed hyps;
  1.1244      val prop1 = attach_tpairs tpairs prop;
  1.1245      val (prop2, al) = Type.varify (prop1, tfrees);
  1.1246 -    val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
  1.1247 -  in (*no fix_shyps*)
  1.1248 -   (Thm{thy_ref = thy_ref,
  1.1249 -        der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
  1.1250 -        maxidx = Int.max(0,maxidx),
  1.1251 -        shyps = shyps,
  1.1252 -        hyps = hyps,
  1.1253 -        tpairs = rev (map Logic.dest_equals ts),
  1.1254 -        prop = prop3}, al)
  1.1255 +    val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1.1256 +  in
  1.1257 +    (Thm {thy_ref = thy_ref,
  1.1258 +      der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
  1.1259 +      maxidx = Int.max (0, maxidx),
  1.1260 +      shyps = shyps,
  1.1261 +      hyps = hyps,
  1.1262 +      tpairs = rev (map Logic.dest_equals ts),
  1.1263 +      prop = prop3}, al)
  1.1264    end;
  1.1265  
  1.1266  val varifyT = #1 o varifyT' [];
  1.1267  
  1.1268  (* Replace all TVars by new TFrees *)
  1.1269 -fun freezeT(Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  1.1270 +fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  1.1271    let
  1.1272      val prop1 = attach_tpairs tpairs prop;
  1.1273      val prop2 = Type.freeze prop1;
  1.1274 -    val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
  1.1275 -  in (*no fix_shyps*)
  1.1276 -    Thm{thy_ref = thy_ref,
  1.1277 -        der = Pt.infer_derivs' (Pt.freezeT prop1) der,
  1.1278 -        maxidx = maxidx_of_term prop2,
  1.1279 -        shyps = shyps,
  1.1280 -        hyps = hyps,
  1.1281 -        tpairs = rev (map Logic.dest_equals ts),
  1.1282 -        prop = prop3}
  1.1283 +    val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1.1284 +  in
  1.1285 +    Thm {thy_ref = thy_ref,
  1.1286 +      der = Pt.infer_derivs' (Pt.freezeT prop1) der,
  1.1287 +      maxidx = maxidx_of_term prop2,
  1.1288 +      shyps = shyps,
  1.1289 +      hyps = hyps,
  1.1290 +      tpairs = rev (map Logic.dest_equals ts),
  1.1291 +      prop = prop3}
  1.1292    end;
  1.1293  
  1.1294  
  1.1295 @@ -1084,105 +1043,108 @@
  1.1296  (*Increment variables and parameters of orule as required for
  1.1297    resolution with goal i of state. *)
  1.1298  fun lift_rule (state, i) orule =
  1.1299 -  let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state
  1.1300 -      val (Bi::_, _) = Logic.strip_prems(i, [], sprop)
  1.1301 -        handle TERM _ => raise THM("lift_rule", i, [orule,state])
  1.1302 -      val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi}
  1.1303 -      val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
  1.1304 -      val (Thm{thy_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule
  1.1305 -      val (As, B) = Logic.strip_horn prop
  1.1306 -  in  (*no fix_shyps*)
  1.1307 -      Thm{thy_ref = merge_thm_thys(state,orule),
  1.1308 -          der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der,
  1.1309 -          maxidx = maxidx+smax+1,
  1.1310 -          shyps = Sorts.union_sort(sshyps,shyps),
  1.1311 -          hyps = hyps,
  1.1312 -          tpairs = map (pairself lift_abs) tpairs,
  1.1313 -          prop = Logic.list_implies (map lift_all As, lift_all B)}
  1.1314 +  let
  1.1315 +    val Thm {shyps = sshyps, prop = sprop, maxidx = smax, thy_ref = sthy_ref,...} = state;
  1.1316 +    val (Bi :: _, _) = Logic.strip_prems (i, [], sprop)
  1.1317 +      handle TERM _ => raise THM ("lift_rule", i, [orule, state]);
  1.1318 +    val (lift_abs, lift_all) = Logic.lift_fns (Bi, smax + 1);
  1.1319 +    val (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = orule;
  1.1320 +    val (As, B) = Logic.strip_horn prop;
  1.1321 +  in
  1.1322 +    Thm {thy_ref = merge_thys2 state orule,
  1.1323 +      der = Pt.infer_derivs' (Pt.lift_proof Bi (smax + 1) prop) der,
  1.1324 +      maxidx = maxidx + smax + 1,
  1.1325 +      shyps = Sorts.union sshyps shyps,
  1.1326 +      hyps = hyps,
  1.1327 +      tpairs = map (pairself lift_abs) tpairs,
  1.1328 +      prop = Logic.list_implies (map lift_all As, lift_all B)}
  1.1329    end;
  1.1330  
  1.1331  fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  1.1332 -  if i < 0 then raise THM ("negative increment", 0, [thm]) else
  1.1333 -  if i = 0 then thm else
  1.1334 +  if i < 0 then raise THM ("negative increment", 0, [thm])
  1.1335 +  else if i = 0 then thm
  1.1336 +  else
  1.1337      Thm {thy_ref = thy_ref,
  1.1338 -         der = Pt.infer_derivs' (Pt.map_proof_terms
  1.1339 -           (Logic.incr_indexes ([], i)) (incr_tvar i)) der,
  1.1340 -         maxidx = maxidx + i,
  1.1341 -         shyps = shyps,
  1.1342 -         hyps = hyps,
  1.1343 -         tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,
  1.1344 -         prop = Logic.incr_indexes ([], i) prop};
  1.1345 +      der = Pt.infer_derivs' (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i)) der,
  1.1346 +      maxidx = maxidx + i,
  1.1347 +      shyps = shyps,
  1.1348 +      hyps = hyps,
  1.1349 +      tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,
  1.1350 +      prop = Logic.incr_indexes ([], i) prop};
  1.1351  
  1.1352  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1.1353  fun assumption i state =
  1.1354 -  let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
  1.1355 -      val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1.1356 -      fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) =
  1.1357 -        fix_shyps [state] (env_codT env)
  1.1358 -          (Thm{thy_ref = thy_ref,
  1.1359 -               der = Pt.infer_derivs'
  1.1360 -                 ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
  1.1361 -                   Pt.assumption_proof Bs Bi n) der,
  1.1362 -               maxidx = maxidx,
  1.1363 -               shyps = [],
  1.1364 -               hyps = hyps,
  1.1365 -               tpairs = if Envir.is_empty env then tpairs else
  1.1366 -                 map (pairself (Envir.norm_term env)) tpairs,
  1.1367 -               prop =
  1.1368 -               if Envir.is_empty env then (*avoid wasted normalizations*)
  1.1369 -                   Logic.list_implies (Bs, C)
  1.1370 -               else (*normalize the new rule fully*)
  1.1371 -                   Envir.norm_term env (Logic.list_implies (Bs, C))});
  1.1372 -      fun addprfs [] _ = Seq.empty
  1.1373 -        | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull
  1.1374 -             (Seq.mapp (newth n)
  1.1375 -                (Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs))
  1.1376 -                (addprfs apairs (n+1))))
  1.1377 -  in  addprfs (Logic.assum_pairs (~1,Bi)) 1 end;
  1.1378 +  let
  1.1379 +    val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state;
  1.1380 +    val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1.1381 +    fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
  1.1382 +      Thm {thy_ref = thy_ref,
  1.1383 +        der = Pt.infer_derivs'
  1.1384 +          ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
  1.1385 +            Pt.assumption_proof Bs Bi n) der,
  1.1386 +        maxidx = maxidx,
  1.1387 +        shyps = insert_env_sorts env shyps,
  1.1388 +        hyps = hyps,
  1.1389 +        tpairs =
  1.1390 +          if Envir.is_empty env then tpairs
  1.1391 +          else map (pairself (Envir.norm_term env)) tpairs,
  1.1392 +        prop =
  1.1393 +          if Envir.is_empty env then (*avoid wasted normalizations*)
  1.1394 +            Logic.list_implies (Bs, C)
  1.1395 +          else (*normalize the new rule fully*)
  1.1396 +            Envir.norm_term env (Logic.list_implies (Bs, C))};
  1.1397 +    fun addprfs [] _ = Seq.empty
  1.1398 +      | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull
  1.1399 +          (Seq.mapp (newth n)
  1.1400 +            (Unify.unifiers (Theory.deref thy_ref, Envir.empty maxidx, (t, u) :: tpairs))
  1.1401 +            (addprfs apairs (n + 1))))
  1.1402 +  in addprfs (Logic.assum_pairs (~1, Bi)) 1 end;
  1.1403  
  1.1404  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1.1405    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  1.1406  fun eq_assumption i state =
  1.1407 -  let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
  1.1408 -      val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1.1409 -  in  (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of
  1.1410 -         (~1) => raise THM("eq_assumption", 0, [state])
  1.1411 -       | n => fix_shyps [state] []
  1.1412 -                (Thm{thy_ref = thy_ref,
  1.1413 -                     der = Pt.infer_derivs'
  1.1414 -                       (Pt.assumption_proof Bs Bi (n+1)) der,
  1.1415 -                     maxidx = maxidx,
  1.1416 -                     shyps = [],
  1.1417 -                     hyps = hyps,
  1.1418 -                     tpairs = tpairs,
  1.1419 -                     prop = Logic.list_implies (Bs, C)}))
  1.1420 +  let
  1.1421 +    val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state;
  1.1422 +    val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1.1423 +  in
  1.1424 +    (case find_index (op aconv) (Logic.assum_pairs (~1, Bi)) of
  1.1425 +      ~1 => raise THM ("eq_assumption", 0, [state])
  1.1426 +    | n =>
  1.1427 +        Thm {thy_ref = thy_ref,
  1.1428 +          der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der,
  1.1429 +          maxidx = maxidx,
  1.1430 +          shyps = shyps,
  1.1431 +          hyps = hyps,
  1.1432 +          tpairs = tpairs,
  1.1433 +          prop = Logic.list_implies (Bs, C)})
  1.1434    end;
  1.1435  
  1.1436  
  1.1437  (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1.1438  fun rotate_rule k i state =
  1.1439 -  let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state;
  1.1440 -      val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1.1441 -      val params = Term.strip_all_vars Bi
  1.1442 -      and rest   = Term.strip_all_body Bi
  1.1443 -      val asms   = Logic.strip_imp_prems rest
  1.1444 -      and concl  = Logic.strip_imp_concl rest
  1.1445 -      val n      = length asms
  1.1446 -      val m      = if k<0 then n+k else k
  1.1447 -      val Bi'    = if 0=m orelse m=n then Bi
  1.1448 -                   else if 0<m andalso m<n
  1.1449 -                   then let val (ps,qs) = splitAt(m,asms)
  1.1450 -                        in list_all(params, Logic.list_implies(qs @ ps, concl))
  1.1451 -                        end
  1.1452 -                   else raise THM("rotate_rule", k, [state])
  1.1453 -  in  (*no fix_shyps*)
  1.1454 -      Thm{thy_ref = thy_ref,
  1.1455 -          der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
  1.1456 -          maxidx = maxidx,
  1.1457 -          shyps = shyps,
  1.1458 -          hyps = hyps,
  1.1459 -          tpairs = tpairs,
  1.1460 -          prop = Logic.list_implies (Bs @ [Bi'], C)}
  1.1461 +  let
  1.1462 +    val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state;
  1.1463 +    val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1.1464 +    val params = Term.strip_all_vars Bi
  1.1465 +    and rest   = Term.strip_all_body Bi;
  1.1466 +    val asms   = Logic.strip_imp_prems rest
  1.1467 +    and concl  = Logic.strip_imp_concl rest;
  1.1468 +    val n = length asms;
  1.1469 +    val m = if k < 0 then n + k else k;
  1.1470 +    val Bi' =
  1.1471 +      if 0 = m orelse m = n then Bi
  1.1472 +      else if 0 < m andalso m < n then
  1.1473 +        let val (ps, qs) = splitAt (m, asms)
  1.1474 +        in list_all (params, Logic.list_implies (qs @ ps, concl)) end
  1.1475 +      else raise THM ("rotate_rule", k, [state]);
  1.1476 +  in
  1.1477 +    Thm {thy_ref = thy_ref,
  1.1478 +      der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
  1.1479 +      maxidx = maxidx,
  1.1480 +      shyps = shyps,
  1.1481 +      hyps = hyps,
  1.1482 +      tpairs = tpairs,
  1.1483 +      prop = Logic.list_implies (Bs @ [Bi'], C)}
  1.1484    end;
  1.1485  
  1.1486  
  1.1487 @@ -1190,27 +1152,29 @@
  1.1488    unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  1.1489    number of premises.  Useful with etac and underlies tactic/defer_tac*)
  1.1490  fun permute_prems j k rl =
  1.1491 -  let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
  1.1492 -      val prems  = Logic.strip_imp_prems prop
  1.1493 -      and concl  = Logic.strip_imp_concl prop
  1.1494 -      val moved_prems = List.drop(prems, j)
  1.1495 -      and fixed_prems = List.take(prems, j)
  1.1496 -        handle Subscript => raise THM("permute_prems:j", j, [rl])
  1.1497 -      val n_j    = length moved_prems
  1.1498 -      val m = if k<0 then n_j + k else k
  1.1499 -      val prop'  = if 0 = m orelse m = n_j then prop
  1.1500 -                   else if 0<m andalso m<n_j
  1.1501 -                   then let val (ps,qs) = splitAt(m,moved_prems)
  1.1502 -                        in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
  1.1503 -                   else raise THM("permute_prems:k", k, [rl])
  1.1504 -  in  (*no fix_shyps*)
  1.1505 -      Thm{thy_ref = thy_ref,
  1.1506 -          der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
  1.1507 -          maxidx = maxidx,
  1.1508 -          shyps = shyps,
  1.1509 -          hyps = hyps,
  1.1510 -          tpairs = tpairs,
  1.1511 -          prop = prop'}
  1.1512 +  let
  1.1513 +    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl;
  1.1514 +    val prems = Logic.strip_imp_prems prop
  1.1515 +    and concl = Logic.strip_imp_concl prop;
  1.1516 +    val moved_prems = List.drop (prems, j)
  1.1517 +    and fixed_prems = List.take (prems, j)
  1.1518 +      handle Subscript => raise THM ("permute_prems: j", j, [rl]);
  1.1519 +    val n_j = length moved_prems;
  1.1520 +    val m = if k < 0 then n_j + k else k;
  1.1521 +    val prop' =
  1.1522 +      if 0 = m orelse m = n_j then prop
  1.1523 +      else if 0 < m andalso m < n_j then
  1.1524 +        let val (ps, qs) = splitAt (m, moved_prems)
  1.1525 +        in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
  1.1526 +      else raise THM ("permute_prems:k", k, [rl]);
  1.1527 +  in
  1.1528 +    Thm {thy_ref = thy_ref,
  1.1529 +      der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
  1.1530 +      maxidx = maxidx,
  1.1531 +      shyps = shyps,
  1.1532 +      hyps = hyps,
  1.1533 +      tpairs = tpairs,
  1.1534 +      prop = prop'}
  1.1535    end;
  1.1536  
  1.1537  
  1.1538 @@ -1221,35 +1185,36 @@
  1.1539    The names in cs, if distinct, are used for the innermost parameters;
  1.1540     preceding parameters may be renamed to make all params distinct.*)
  1.1541  fun rename_params_rule (cs, i) state =
  1.1542 -  let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state
  1.1543 -      val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1.1544 -      val iparams = map #1 (Logic.strip_params Bi)
  1.1545 -      val short = length iparams - length cs
  1.1546 -      val newnames =
  1.1547 -            if short<0 then error"More names than abstractions!"
  1.1548 -            else variantlist(Library.take (short,iparams), cs) @ cs
  1.1549 -      val freenames = map (#1 o dest_Free) (term_frees Bi)
  1.1550 -      val newBi = Logic.list_rename_params (newnames, Bi)
  1.1551 +  let
  1.1552 +    val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state;
  1.1553 +    val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1.1554 +    val iparams = map #1 (Logic.strip_params Bi);
  1.1555 +    val short = length iparams - length cs;
  1.1556 +    val newnames =
  1.1557 +      if short < 0 then error "More names than abstractions!"
  1.1558 +      else variantlist (Library.take (short, iparams), cs) @ cs;
  1.1559 +    val freenames = map (#1 o dest_Free) (term_frees Bi);
  1.1560 +    val newBi = Logic.list_rename_params (newnames, Bi);
  1.1561    in
  1.1562 -  case findrep cs of
  1.1563 -     c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c);
  1.1564 -              state)
  1.1565 -   | [] => (case cs inter_string freenames of
  1.1566 -       a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a);
  1.1567 -                state)
  1.1568 -     | [] => Thm{thy_ref = thy_ref,
  1.1569 -                 der = der,
  1.1570 -                 maxidx = maxidx,
  1.1571 -                 shyps = shyps,
  1.1572 -                 hyps = hyps,
  1.1573 -                 tpairs = tpairs,
  1.1574 -                 prop = Logic.list_implies (Bs @ [newBi], C)})
  1.1575 +    case findrep cs of
  1.1576 +      c :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
  1.1577 +    | [] =>
  1.1578 +      (case cs inter_string freenames of
  1.1579 +        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
  1.1580 +      | [] =>
  1.1581 +        Thm {thy_ref = thy_ref,
  1.1582 +          der = der,
  1.1583 +          maxidx = maxidx,
  1.1584 +          shyps = shyps,
  1.1585 +          hyps = hyps,
  1.1586 +          tpairs = tpairs,
  1.1587 +          prop = Logic.list_implies (Bs @ [newBi], C)})
  1.1588    end;
  1.1589  
  1.1590  
  1.1591  (*** Preservation of bound variable names ***)
  1.1592  
  1.1593 -fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
  1.1594 +fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  1.1595    (case Term.rename_abs pat obj prop of
  1.1596      NONE => thm
  1.1597    | SOME prop' => Thm
  1.1598 @@ -1344,7 +1309,7 @@
  1.1599           (*How many hyps to skip over during normalization*)
  1.1600       and nlift = Logic.count_prems(strip_all_body Bi,
  1.1601                                     if eres_flg then ~1 else 0)
  1.1602 -     val thy_ref = merge_thm_thys(state,orule);
  1.1603 +     val thy_ref = merge_thys2 state orule;
  1.1604       val thy = Theory.deref thy_ref;
  1.1605       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  1.1606       fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
  1.1607 @@ -1363,7 +1328,7 @@
  1.1608                  else (*normalize the new rule fully*)
  1.1609                    (ntps, (map normt (Bs @ As), normt C))
  1.1610               end
  1.1611 -           val th = (*tuned fix_shyps*)
  1.1612 +           val th =
  1.1613               Thm{thy_ref = thy_ref,
  1.1614                   der = Pt.infer_derivs
  1.1615                     ((if Envir.is_empty env then I
  1.1616 @@ -1373,8 +1338,8 @@
  1.1617                         curry op oo (Pt.norm_proof' env))
  1.1618                      (Pt.bicompose_proof Bs oldAs As A n)) rder' sder,
  1.1619                   maxidx = maxidx,
  1.1620 -                 shyps = add_env_sorts (env, Sorts.union_sort(rshyps,sshyps)),
  1.1621 -                 hyps = union_term(rhyps,shyps),
  1.1622 +                 shyps = insert_env_sorts env (Sorts.union rshyps sshyps),
  1.1623 +                 hyps = union_hyps rhyps shyps,
  1.1624                   tpairs = ntpairs,
  1.1625                   prop = Logic.list_implies normp}
  1.1626          in  Seq.cons(th, thq)  end  handle COMPOSE => thq;
  1.1627 @@ -1464,14 +1429,14 @@
  1.1628        in
  1.1629          if T <> propT then
  1.1630            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  1.1631 -        else fix_shyps [] []
  1.1632 -          (Thm {thy_ref = Theory.self_ref thy',
  1.1633 +        else
  1.1634 +          Thm {thy_ref = Theory.self_ref thy',
  1.1635              der = (true, Pt.oracle_proof name prop),
  1.1636              maxidx = maxidx,
  1.1637 -            shyps = [],
  1.1638 +            shyps = Sorts.insert_term prop [],
  1.1639              hyps = [],
  1.1640              tpairs = [],
  1.1641 -            prop = prop})
  1.1642 +            prop = prop}
  1.1643        end
  1.1644    end;
  1.1645