--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Aug 17 18:05:31 2011 +0200
@@ -102,16 +102,16 @@
let
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
in
- absdummy (@{typ nat}, absdummy (@{typ nat},
- Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
+ absdummy @{typ nat} (absdummy @{typ nat}
+ (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
(@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
Predicate_Compile_Aux.mk_single compfuns
(@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
end
fun enumerate_addups_nat compfuns (_ : typ) =
- absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
- (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
+ absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
+ (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $
(@{term "Code_Numeral.nat_of"} $ Bound 0) $
(@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
@{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
@@ -120,8 +120,8 @@
val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
in
- absdummy(@{typ nat}, absdummy (@{typ nat},
- Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
+ absdummy @{typ nat} (absdummy @{typ nat}
+ (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
(@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
(Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
@{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $