103 fun ren t = the_default t (Term.rename_abs tm1 tm t); |
103 fun ren t = the_default t (Term.rename_abs tm1 tm t); |
104 val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); |
104 val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); |
105 val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); |
105 val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); |
106 val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; |
106 val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; |
107 val env' = Envir.Envir |
107 val env' = Envir.Envir |
108 {maxidx = Library.foldl Int.max |
108 {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1, |
109 (~1, map (Int.max o pairself maxidx_of_term) prems'), |
109 tenv = tenv, tyenv = Tenv}; |
110 iTs = Tenv, asol = tenv}; |
|
111 val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env'; |
110 val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env'; |
112 in SOME (Envir.norm_term env'' (inc (ren tm2))) |
111 in SOME (Envir.norm_term env'' (inc (ren tm2))) |
113 end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) |
112 end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) |
114 (sort (int_ord o pairself fst) |
113 (sort (int_ord o pairself fst) |
115 (Net.match_term rules (Envir.eta_contract tm))) |
114 (Net.match_term rules (Envir.eta_contract tm))) |