# HG changeset patch # User wenzelm # Date 1247859180 -7200 # Node ID a6a6e8031c14b7e233375e39d42b0b0c27fa88a8 # Parent e2e6b0691264f56be1e0d93f92f891eabea2d5f3 tuned/modernized Envir operations; diff -r e2e6b0691264 -r a6a6e8031c14 src/HOL/Library/reflection.ML --- 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)) diff -r e2e6b0691264 -r a6a6e8031c14 src/HOL/Tools/meson.ML --- 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 diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/Isar/proof_context.ML --- 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 *) diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/Proof/extraction.ML --- 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) diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/Proof/reconstruct.ML --- 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; diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/pattern.ML --- 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)) => diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/proofterm.ML --- 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; diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/thm.ML --- 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, diff -r e2e6b0691264 -r a6a6e8031c14 src/Pure/unify.ML --- 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'; diff -r e2e6b0691264 -r a6a6e8031c14 src/Tools/eqsubst.ML --- 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; diff -r e2e6b0691264 -r a6a6e8031c14 src/Tools/induct.ML --- 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;