--- a/src/HOL/Library/reflection.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/HOL/Library/reflection.ML Fri Jul 17 21:33:00 2009 +0200
@@ -153,8 +153,8 @@
val certy = ctyp_of thy
val (tyenv, tmenv) =
Pattern.match thy
- ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
+ ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
+ (Vartab.empty, Vartab.empty)
val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
val (fts,its) =
(map (snd o snd) fnvs,
@@ -204,9 +204,7 @@
val xns_map = (fst (split_list nths)) ~~ xns
val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
val rhs_P = subst_free subst rhs
- val (tyenv, tmenv) = Pattern.match
- thy (rhs_P, t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
+ val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
val sbst = Envir.subst_vars (tyenv, tmenv)
val sbsT = Envir.typ_subst_TVars tyenv
val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
--- a/src/HOL/Tools/meson.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jul 17 21:33:00 2009 +0200
@@ -87,14 +87,12 @@
fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
-val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
-
(*FIXME: currently does not "rename variables apart"*)
fun first_order_resolve thA thB =
let val thy = theory_of_thm thA
val tmA = concl_of thA
val Const("==>",_) $ tmB $ _ = prop_of thB
- val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
+ val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
in thA RS (cterm_instantiate ct_pairs thB) end
handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *)
@@ -104,8 +102,8 @@
[] => th
| pairs =>
let val thy = theory_of_thm th
- val (tyenv,tenv) =
- List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
+ val (tyenv, tenv) =
+ fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
val t_pairs = map term_pair_of (Vartab.dest tenv)
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
in th' end
--- a/src/Pure/Isar/proof_context.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jul 17 21:33:00 2009 +0200
@@ -779,7 +779,7 @@
fun simult_matches ctxt (t, pats) =
(case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
NONE => error "Pattern match failed!"
- | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
+ | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
(* bind_terms *)
--- a/src/Pure/Proof/extraction.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jul 17 21:33:00 2009 +0200
@@ -105,9 +105,8 @@
val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
val env' = Envir.Envir
- {maxidx = Library.foldl Int.max
- (~1, map (Int.max o pairself maxidx_of_term) prems'),
- iTs = Tenv, asol = tenv};
+ {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
+ tenv = tenv, tyenv = Tenv};
val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
in SOME (Envir.norm_term env'' (inc (ren tm2)))
end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
--- a/src/Pure/Proof/reconstruct.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Jul 17 21:33:00 2009 +0200
@@ -35,12 +35,6 @@
fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
(vars_of prop @ frees_of prop) prf;
-fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
- (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
- Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
- iTs=Vartab.merge (op =) (iTs1, iTs2),
- maxidx=Int.max (maxidx1, maxidx2)};
-
(**** generate constraints for proof term ****)
@@ -48,31 +42,32 @@
let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
-fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) =
- (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
- TVar (("'t", maxidx+1), s));
+fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
+ (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
+ TVar (("'t", maxidx + 1), s));
val mk_abs = fold (fn T => fn u => Abs ("", T, u));
fun unifyT thy env T U =
let
- val Envir.Envir {asol, iTs, maxidx} = env;
- val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
- in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
- handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
- Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
+ val Envir.Envir {maxidx, tenv, tyenv} = env;
+ val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
-fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
- (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
+fun chaseT env (T as TVar v) =
+ (case Type.lookup (Envir.type_env env) v of
+ NONE => T
+ | SOME T' => chaseT env T')
| chaseT _ T = T;
-fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
- (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
+ (t as Const (s, T)) = if T = dummyT then
+ (case Sign.const_type thy s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
| SOME T =>
let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
in (Const (s, T'), T', vTs,
- Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
+ Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
end)
else (t, T, vTs, env)
| infer_type thy env Ts vTs (t as Free (s, T)) =
@@ -236,21 +231,23 @@
fun upd_constrs env cs =
let
- val Envir.Envir {asol, iTs, ...} = env;
+ val tenv = Envir.term_env env;
+ val tyenv = Envir.type_env env;
val dom = []
- |> Vartab.fold (cons o #1) asol
- |> Vartab.fold (cons o #1) iTs;
+ |> Vartab.fold (cons o #1) tenv
+ |> Vartab.fold (cons o #1) tyenv;
val vran = []
- |> Vartab.fold (Term.add_var_names o #2 o #2) asol
- |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
+ |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
+ |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
fun check_cs [] = []
- | check_cs ((u, p, vs)::ps) =
- let val vs' = subtract (op =) dom vs;
- in if vs = vs' then (u, p, vs)::check_cs ps
- else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
- end
+ | check_cs ((u, p, vs) :: ps) =
+ let val vs' = subtract (op =) dom vs in
+ if vs = vs' then (u, p, vs) :: check_cs ps
+ else (true, p, fold (insert op =) vs' vran) :: check_cs ps
+ end;
in check_cs cs end;
+
(**** solution of constraints ****)
fun solve _ [] bigenv = bigenv
@@ -280,7 +277,7 @@
val Envir.Envir {maxidx, ...} = bigenv;
val (env, cs') = search (Envir.empty maxidx) cs;
in
- solve thy (upd_constrs env cs') (merge_envs bigenv env)
+ solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
end;
--- a/src/Pure/pattern.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/pattern.ML Fri Jul 17 21:33:00 2009 +0200
@@ -141,8 +141,10 @@
| split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
| split_type _ = error("split_type");
-fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
- let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
+fun type_of_G env (T, n, is) =
+ let
+ val tyenv = Envir.type_env env;
+ val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
in map (nth Ts) is ---> U end;
fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
@@ -225,11 +227,12 @@
end;
in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
-fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
- if T=U then env
- else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
- in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
- handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
+fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
+ if T = U then env
+ else
+ let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+ handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
--- a/src/Pure/proofterm.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 17 21:33:00 2009 +0200
@@ -489,9 +489,8 @@
| remove_types (Const (s, _)) = Const (s, dummyT)
| remove_types t = t;
-fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
- Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
- maxidx = maxidx};
+fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
+ Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
--- a/src/Pure/thm.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/thm.ML Fri Jul 17 21:33:00 2009 +0200
@@ -1247,12 +1247,12 @@
val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
val thy = Theory.deref thy_ref;
val (tpairs, Bs, Bi, C) = dest_state (state, i);
- fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
+ fun newth n (env, tpairs) =
Thm (deriv_rule1
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
Pt.assumption_proof Bs Bi n) der,
{tags = [],
- maxidx = maxidx,
+ maxidx = Envir.maxidx_of env,
shyps = Envir.insert_sorts env shyps,
hyps = hyps,
tpairs =
@@ -1465,15 +1465,15 @@
(*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' = Envir.typ_subst_TVars iTs T
- (*Must instantiate types of parameters because they are flattened;
- this could be a NEW parameter*)
- in Term.all T' $ Abs(a, T', norm_term_skip env n t) end
- | norm_term_skip env n (Const("==>", _) $ A $ B) =
- Logic.mk_implies (A, norm_term_skip env (n-1) B)
- | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
+ | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
+ let
+ val T' = Envir.typ_subst_TVars (Envir.type_env env) T
+ (*Must instantiate types of parameters because they are flattened;
+ this could be a NEW parameter*)
+ in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
+ | norm_term_skip env n (Const ("==>", _) $ A $ B) =
+ Logic.mk_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)
@@ -1495,7 +1495,7 @@
and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
val thy = Theory.deref (merge_thys2 state orule);
(** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
- fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
+ fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
let val normt = Envir.norm_term env;
(*perform minimal copying here by examining env*)
val (ntpairs, normp) =
@@ -1520,7 +1520,7 @@
curry op oo (Pt.norm_proof' env))
(Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
{tags = [],
- maxidx = maxidx,
+ maxidx = Envir.maxidx_of env,
shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
hyps = union_hyps rhyps shyps,
tpairs = ntpairs,
--- a/src/Pure/unify.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/unify.ML Fri Jul 17 21:33:00 2009 +0200
@@ -52,36 +52,48 @@
type dpair = binderlist * term * term;
-fun body_type(Envir.Envir{iTs,...}) =
-let fun bT(Type("fun",[_,T])) = bT T
- | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
- NONE => T | SOME(T') => bT T')
- | bT T = T
-in bT end;
+fun body_type env =
+ let
+ val tyenv = Envir.type_env env;
+ fun bT (Type ("fun", [_, T])) = bT T
+ | bT (T as TVar v) =
+ (case Type.lookup tyenv v of
+ NONE => T
+ | SOME T' => bT T')
+ | bT T = T;
+ in bT end;
-fun binder_types(Envir.Envir{iTs,...}) =
-let fun bTs(Type("fun",[T,U])) = T :: bTs U
- | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
- NONE => [] | SOME(T') => bTs T')
- | bTs _ = []
-in bTs end;
+fun binder_types env =
+ let
+ val tyenv = Envir.type_env env;
+ fun bTs (Type ("fun", [T, U])) = T :: bTs U
+ | bTs (T as TVar v) =
+ (case Type.lookup tyenv v of
+ NONE => []
+ | SOME T' => bTs T')
+ | bTs _ = [];
+ in bTs end;
fun strip_type env T = (binder_types env T, body_type env T);
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
-(*Eta normal form*)
-fun eta_norm(env as Envir.Envir{iTs,...}) =
- let fun etif (Type("fun",[T,U]), t) =
- Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
- | etif (TVar ixnS, t) =
- (case Type.lookup iTs ixnS of
- NONE => t | SOME(T) => etif(T,t))
- | etif (_,t) = t;
- fun eta_nm (rbinder, Abs(a,T,body)) =
- Abs(a, T, eta_nm ((a,T)::rbinder, body))
- | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
+(* eta normal form *)
+
+fun eta_norm env =
+ let
+ val tyenv = Envir.type_env env;
+ fun etif (Type ("fun", [T, U]), t) =
+ Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
+ | etif (TVar v, t) =
+ (case Type.lookup tyenv v of
+ NONE => t
+ | SOME T => etif (T, t))
+ | etif (_, t) = t;
+ fun eta_nm (rbinder, Abs (a, T, body)) =
+ Abs (a, T, eta_nm ((a, T) :: rbinder, body))
+ | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
in eta_nm end;
@@ -186,11 +198,14 @@
exception ASSIGN; (*Raised if not an assignment*)
-fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
- if T=U then env
- else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
- in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
- handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy (T, U, env) =
+ if T = U then env
+ else
+ let
+ val Envir.Envir {maxidx, tenv, tyenv} = env;
+ val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+ handle Type.TUNIFY => raise CANTUNIFY;
fun test_unify_types thy (args as (T,U,_)) =
let val str_of = Syntax.string_of_typ_global thy;
@@ -636,9 +651,9 @@
(*Pattern matching*)
-fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
+fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
- in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
+ in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
handle Pattern.MATCH => Seq.empty;
(*General matching -- keeps variables disjoint*)
@@ -661,10 +676,12 @@
Term.map_aterms (fn t as Var ((x, i), T) =>
if i > maxidx then Var ((x, i - offset), T) else t | t => t);
- fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
- ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
- fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
+ fun norm_tvar env ((x, i), S) =
+ ((x, i - offset),
+ (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
+ fun norm_var env ((x, i), T) =
let
+ val tyenv = Envir.type_env env;
val T' = Envir.norm_type tyenv T;
val t' = Envir.norm_term env (Var ((x, i), T'));
in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
@@ -672,8 +689,8 @@
fun result env =
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *)
SOME (Envir.Envir {maxidx = maxidx,
- iTs = Vartab.make (map (norm_tvar env) pat_tvars),
- asol = Vartab.make (map (norm_var env) pat_vars)})
+ tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
+ tenv = Vartab.make (map (norm_var env) pat_vars)})
else NONE;
val empty = Envir.empty maxidx';
--- a/src/Tools/eqsubst.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Tools/eqsubst.ML Fri Jul 17 21:33:00 2009 +0200
@@ -231,9 +231,9 @@
or should I be using them somehow? *)
fun mk_insts env =
(Vartab.dest (Envir.type_env env),
- Envir.alist_of env);
- val initenv = Envir.Envir {asol = Vartab.empty,
- iTs = typinsttab, maxidx = ix2};
+ Vartab.dest (Envir.term_env env));
+ val initenv =
+ Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
val useq = Unify.smash_unifiers thry [a] initenv
handle UnequalLengths => Seq.empty
| Term.TERM _ => Seq.empty;
--- a/src/Tools/induct.ML Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Tools/induct.ML Fri Jul 17 21:33:00 2009 +0200
@@ -423,14 +423,15 @@
local
-fun dest_env thy (env as Envir.Envir {iTs, ...}) =
+fun dest_env thy env =
let
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
- val pairs = Envir.alist_of env;
+ val pairs = Vartab.dest (Envir.term_env env);
+ val types = Vartab.dest (Envir.type_env env);
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
- in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
+ in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
in
@@ -450,8 +451,7 @@
val rule' = Thm.incr_indexes (maxidx + 1) rule;
val concl = Logic.strip_assums_concl goal;
in
- Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
- (Envir.empty (#maxidx (Thm.rep_thm rule')))
+ Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
|> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
end
end handle Subscript => Seq.empty;