src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 51143 0a2371e7ced3
parent 50046 0051dc4f301f
child 51672 d5c5e088ebdf
child 51685 385ef6706252
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -70,8 +70,8 @@
     1.4  fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
     1.5    let
     1.6      val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
     1.7 -    val narrowing_term = @{term "Quickcheck_Narrowing.Narrowing_constructor"} $ HOLogic.mk_number @{typ code_int} i
     1.8 -      $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
     1.9 +    val narrowing_term = @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i
    1.10 +      $ HOLogic.mk_list @{typ narrowing_term} (rev frees)
    1.11      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    1.12          (map mk_partial_term_of (frees ~~ tys))
    1.13          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
    1.14 @@ -124,7 +124,7 @@
    1.15  val narrowingN = "narrowing";
    1.16  
    1.17  fun narrowingT T =
    1.18 -  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
    1.19 +  @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
    1.20  
    1.21  fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
    1.22