--- a/src/HOL/Tools/inductive.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Dec 02 14:54:25 2011 +0100
@@ -128,7 +128,7 @@
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
fun make_bool_args' xs =
- make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
+ make_bool_args (K @{term False}) (K @{term True}) xs;
fun arg_types_of k c = drop k (binder_types (fastype_of c));
@@ -786,14 +786,14 @@
in
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
(Logic.strip_params r)
- (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
+ (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
end;
(* make a disjunction of all introduction rules *)
val fp_fun =
fold_rev lambda (p :: bs @ xs)
- (if null intr_ts then HOLogic.false_const
+ (if null intr_ts then @{term False}
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
(* add definiton of recursive predicates to theory *)