src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 40054 cd7b1fa20bce
parent 39650 2a35950ec495
child 40548 54eb5fd36e5e
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:10 2010 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:11 2010 +0200
     1.3 @@ -96,8 +96,8 @@
     1.4    val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
     1.5    val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
     1.6    val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
     1.7 -  val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
     1.8 -  val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
     1.9 +  val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
    1.10 +  val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
    1.11    fun subtract_nat compfuns (_ : typ) =
    1.12      let
    1.13        val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
    1.14 @@ -128,21 +128,21 @@
    1.15              (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
    1.16      end
    1.17  in
    1.18 -  Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
    1.19 +  Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
    1.20      [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
    1.21       (ooi, (enumerate_addups_nat, false))]
    1.22    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.23         (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
    1.24 -  #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
    1.25 +  #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
    1.26         [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
    1.27    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.28        (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
    1.29 -  #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
    1.30 +  #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
    1.31      [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
    1.32       (oii, (@{const_name subtract}, false))]
    1.33    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.34         (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
    1.35 -  #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
    1.36 +  #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
    1.37      [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
    1.38       (ioi, (@{const_name minus}, false))]
    1.39    #> Predicate_Compile_Fun.add_function_predicate_translation