src/HOL/Nominal/nominal_inductive.ML
changeset 46218 ecf6375e2abb
parent 44929 1886cddaf8a5
child 46947 b8c7eb0c2f89
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 14 19:06:05 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 14 20:05:58 2012 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4             HOLogic.mk_Trueprop (lift_pred p ts));
     1.5          val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
     1.6        in
     1.7 -        (list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
     1.8 +        (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
     1.9        end) prems);
    1.10  
    1.11      val ind_vars =
    1.12 @@ -259,7 +259,7 @@
    1.13          lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls));
    1.14  
    1.15      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    1.16 -      map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    1.17 +      map (fn q => Logic.list_all (params, incr_boundvars ~1 (Logic.list_implies
    1.18            (map_filter (fn prem =>
    1.19               if null (preds_of ps prem) then SOME prem
    1.20               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    1.21 @@ -439,9 +439,9 @@
    1.22        map (fn (prem, args, concl, (prems, _)) =>
    1.23          let
    1.24            fun mk_prem (ps, [], _, prems) =
    1.25 -                list_all (ps, Logic.list_implies (prems, concl))
    1.26 +                Logic.list_all (ps, Logic.list_implies (prems, concl))
    1.27              | mk_prem (ps, qs, _, prems) =
    1.28 -                list_all (ps, Logic.mk_implies
    1.29 +                Logic.list_all (ps, Logic.mk_implies
    1.30                    (Logic.list_implies
    1.31                      (mk_distinct qs @
    1.32                       maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop