diff -r f92919b141b2 -r 42ff710d432f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/HOL.thy	Sat Feb 25 15:19:47 2006 +0100
@@ -1407,23 +1407,7 @@
   uminus "HOL.uminus"
   arbitrary "HOL.arbitrary"
 
-code_syntax_tyco bool
-  ml (target_atom "bool")
-  haskell (target_atom "Bool")
-
 code_syntax_const
-  Not
-    ml (target_atom "not")
-    haskell (target_atom "not")
-  "op &"
-    ml (infixl 1 "andalso")
-    haskell (infixl 3 "&&")
-  "op |"
-    ml (infixl 0 "orelse")
-    haskell (infixl 2 "||")
-  If
-    ml (target_atom "(if __/ then __/ else __)")
-    haskell (target_atom "(if __/ then __/ else __)")
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")