adapted seralizer syntax
authorhaftmann
Tue, 31 Oct 2006 14:58:14 +0100
changeset 21126 4dbc3ccbaab0
parent 21125 9b7d35ca1eef
child 21127 c8e862897d13
adapted seralizer syntax
src/HOL/Datatype.thy
src/HOL/List.thy
--- a/src/HOL/Datatype.thy	Tue Oct 31 14:58:12 2006 +0100
+++ b/src/HOL/Datatype.thy	Tue Oct 31 14:58:14 2006 +0100
@@ -773,18 +773,18 @@
 code_const True and False and Not and "op &" and "op |" and If
   (SML "true" and "false" and "not"
     and infixl 1 "andalso" and infixl 0 "orelse"
-    and "!(if __/ then __/ else __)")
+    and "!(if (_)/ then (_)/ else (_))")
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
-    and "!(if __/ then __/ else __)")
+    and "!(if (_)/ then (_)/ else (_))")
 
 code_type *
   (SML infix 2 "*")
-  (Haskell "!(__,/ __)")
+  (Haskell "!((_),/ (_))")
 
 code_const Pair
-  (SML "!(__,/ __)")
-  (Haskell "!(__,/ __)")
+  (SML "!((_),/ (_))")
+  (Haskell "!((_),/ (_))")
 
 code_type unit
   (SML "unit")
--- a/src/HOL/List.thy	Tue Oct 31 14:58:12 2006 +0100
+++ b/src/HOL/List.thy	Tue Oct 31 14:58:14 2006 +0100
@@ -2662,8 +2662,8 @@
   (Haskell "Char")
 
 code_const Char
-  (SML "!(__,/ __)")
-  (Haskell "!(__,/ __)")
+  (SML "!((_),/ (_))")
+  (Haskell "!((_),/ (_))")
 
 code_instance list :: eq and char :: eq
   (Haskell - and -)