# HG changeset patch
# User haftmann
# Date 1140019765 -3600
# Node ID 1a8f08f9f8afbfe8efd6d89efdb60bb3760936ba
# Parent  88d25a6c346a28d29c0b307ea087939dc7195596
some fixes

diff -r 88d25a6c346a -r 1a8f08f9f8af src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Feb 15 17:09:06 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Wed Feb 15 17:09:25 2006 +0100
@@ -68,8 +68,8 @@
   haskell (target_atom "0")
 
 code_syntax_const Suc
-  ml (infixl 8 "_ + 1")
-  haskell (infixl 6 "_ + 1")
+  ml (target_atom "(__ + 1)")
+  haskell (target_atom "(__ + 1)")
 
 text {*
 Case analysis on natural numbers is rephrased using a conditional
diff -r 88d25a6c346a -r 1a8f08f9f8af src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Feb 15 17:09:06 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Feb 15 17:09:25 2006 +0100
@@ -83,32 +83,32 @@
   "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
 
 code_syntax_const "insert"
-  ml ("{*insert_*} _ _")
-  haskell ("{*insert_*} _ _")
+  ml ("{*insert_*}")
+  haskell ("{*insert_*}")
 
 code_syntax_const "op Un"
-  ml ("{*foldr insert_*} _ _")
-  haskell ("{*foldr insert_*} _ _")
+  ml ("{*foldr insert_*}")
+  haskell ("{*foldr insert_*}")
 
 code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  ml ("{*(flip o foldr) remove*} _ _")
-  haskell ("{*(flip o foldr) remove*} _ _")
+  ml ("{*(flip o foldr) remove*}")
+  haskell ("{*(flip o foldr) remove*}")
 
 code_syntax_const "op Int"
-  ml ("{*inter*} _ _")
-  haskell ("{*inter*} _ _")
+  ml ("{*inter*}")
+  haskell ("{*inter*}")
 
 code_syntax_const "image"
-  ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
-  haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
+  ml ("{*\<lambda>f. foldr (insert_ o f)*}")
+  haskell ("{*\<lambda>f. foldr (insert_ o f)*}")
 
 code_syntax_const "INTER"
-  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
-  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
+  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
+  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
 
 code_syntax_const "UNION"
-  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
-  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
+  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
+  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
 
 code_primconst "Ball"
 ml {*