src/HOL/Quickcheck_Narrowing.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 55147 bce3dbc11f95
--- a/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -13,14 +13,10 @@
 
 setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
 
-code_type typerep
-  (Haskell_Quickcheck "Typerep")
-
-code_const Typerep.Typerep
-  (Haskell_Quickcheck "Typerep")
-
-code_type integer
-  (Haskell_Quickcheck "Prelude.Int")
+code_printing
+  type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
+| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
+| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
 
 code_reserved Haskell_Quickcheck Typerep
 
@@ -47,19 +43,19 @@
 
 consts nth :: "'a list => integer => 'a"
 
-code_const nth (Haskell_Quickcheck infixl 9  "!!")
+code_printing constant nth \<rightharpoonup> (Haskell_Quickcheck) infixl 9 "!!"
 
 consts error :: "char list => 'a"
 
-code_const error (Haskell_Quickcheck "error")
+code_printing constant error \<rightharpoonup> (Haskell_Quickcheck) "error"
 
 consts toEnum :: "integer => char"
 
-code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
+code_printing constant toEnum \<rightharpoonup> (Haskell_Quickcheck) "Prelude.toEnum"
 
 consts marker :: "char"
 
-code_const marker (Haskell_Quickcheck "''\\0'")
+code_printing constant marker \<rightharpoonup> (Haskell_Quickcheck) "''\\0'"
 
 subsubsection {* Narrowing's basic operations *}