--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Oct 21 19:13:11 2010 +0200
@@ -96,8 +96,8 @@
val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
- val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
- val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
+ val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
+ val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
fun subtract_nat compfuns (_ : typ) =
let
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
@@ -128,21 +128,21 @@
(single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
end
in
- Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
+ Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
[(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
(ooi, (enumerate_addups_nat, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
- #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
+ #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
[(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
- #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
+ #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
[(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
(oii, (@{const_name subtract}, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
- #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
+ #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
[(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
(ioi, (@{const_name minus}, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation