src/HOL/Quickcheck_Narrowing.thy
changeset 48565 7c497a239007
parent 48253 4410a709913c
child 48891 c0eafbd55de3
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 20:05:56 2012 +0200
@@ -165,7 +165,7 @@
   false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
 
 code_type code_int
-  (Haskell_Quickcheck "Int")
+  (Haskell_Quickcheck "Prelude.Int")
 
 code_const "0 \<Colon> code_int"
   (Haskell_Quickcheck "0")
@@ -222,7 +222,7 @@
 
 consts toEnum :: "code_int => char"
 
-code_const toEnum (Haskell_Quickcheck "toEnum")
+code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
 
 consts marker :: "char"