src/HOL/Tools/inductive.ML
changeset 45740 132a3e1c0fe5
parent 45652 18214436e1d3
child 46215 0da9433f959e
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 02 14:37:25 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Dec 02 14:54:25 2011 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4        (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
     1.5  
     1.6  fun make_bool_args' xs =
     1.7 -  make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
     1.8 +  make_bool_args (K @{term False}) (K @{term True}) xs;
     1.9  
    1.10  fun arg_types_of k c = drop k (binder_types (fastype_of c));
    1.11  
    1.12 @@ -786,14 +786,14 @@
    1.13        in
    1.14          fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
    1.15            (Logic.strip_params r)
    1.16 -          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
    1.17 +          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
    1.18        end;
    1.19  
    1.20      (* make a disjunction of all introduction rules *)
    1.21  
    1.22      val fp_fun =
    1.23        fold_rev lambda (p :: bs @ xs)
    1.24 -        (if null intr_ts then HOLogic.false_const
    1.25 +        (if null intr_ts then @{term False}
    1.26           else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
    1.27  
    1.28      (* add definiton of recursive predicates to theory *)