src/HOL/HOL.thy
changeset 18757 f0d901bc0686
parent 18708 4b3dadb4fe33
child 18832 6ab4de872a70
--- a/src/HOL/HOL.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -1377,13 +1377,13 @@
   uminus "HOL.uminus"
 
 code_syntax_tyco bool
-  ml (atom "bool")
-  haskell (atom "Bool")
+  ml (target_atom "bool")
+  haskell (target_atom "Bool")
 
 code_syntax_const
   Not
-    ml (atom "not")
-    haskell (atom "not")
+    ml (target_atom "not")
+    haskell (target_atom "not")
   "op &"
     ml (infixl 1 "andalso")
     haskell (infixl 3 "&&")