src/HOL/Nominal/nominal_inductive.ML
changeset 81541 5335b1ca6233
parent 81516 31b05aef022d
equal deleted inserted replaced
81540:58073f3d748a 81541:5335b1ca6233
   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 =