src/HOL/Quickcheck_Narrowing.thy
changeset 48565 7c497a239007
parent 48253 4410a709913c
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 19:27:21 2012 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 20:05:56 2012 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4    false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
     1.5  
     1.6  code_type code_int
     1.7 -  (Haskell_Quickcheck "Int")
     1.8 +  (Haskell_Quickcheck "Prelude.Int")
     1.9  
    1.10  code_const "0 \<Colon> code_int"
    1.11    (Haskell_Quickcheck "0")
    1.12 @@ -222,7 +222,7 @@
    1.13  
    1.14  consts toEnum :: "code_int => char"
    1.15  
    1.16 -code_const toEnum (Haskell_Quickcheck "toEnum")
    1.17 +code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
    1.18  
    1.19  consts marker :: "char"
    1.20