equal
deleted
inserted
replaced
243 (map mk_fresh bvars @ mk_distinct bvars @ |
243 (map mk_fresh bvars @ mk_distinct bvars @ |
244 map (fn prem => |
244 map (fn prem => |
245 if null (preds_of ps prem) then prem |
245 if null (preds_of ps prem) then prem |
246 else lift_prem prem) prems, |
246 else lift_prem prem) prems, |
247 HOLogic.mk_Trueprop (lift_pred p ts)); |
247 HOLogic.mk_Trueprop (lift_pred p ts)); |
248 val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params') |
248 val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds prem params') |
249 in |
249 in |
250 (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem))) |
250 (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem))) |
251 end) prems); |
251 end) prems); |
252 |
252 |
253 val ind_vars = |
253 val ind_vars = |