1.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Feb 15 17:09:06 2006 +0100
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Feb 15 17:09:25 2006 +0100
     1.3 @@ -68,8 +68,8 @@
     1.4    haskell (target_atom "0")
     1.5  
     1.6  code_syntax_const Suc
     1.7 -  ml (infixl 8 "_ + 1")
     1.8 -  haskell (infixl 6 "_ + 1")
     1.9 +  ml (target_atom "(__ + 1)")
    1.10 +  haskell (target_atom "(__ + 1)")
    1.11  
    1.12  text {*
    1.13  Case analysis on natural numbers is rephrased using a conditional

     2.1 --- a/src/HOL/Library/ExecutableSet.thy	Wed Feb 15 17:09:06 2006 +0100
     2.2 +++ b/src/HOL/Library/ExecutableSet.thy	Wed Feb 15 17:09:25 2006 +0100
     2.3 @@ -83,32 +83,32 @@
     2.4    "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
     2.5  
     2.6  code_syntax_const "insert"
     2.7 -  ml ("{*insert_*} _ _")
     2.8 -  haskell ("{*insert_*} _ _")
     2.9 +  ml ("{*insert_*}")
    2.10 +  haskell ("{*insert_*}")
    2.11  
    2.12  code_syntax_const "op Un"
    2.13 -  ml ("{*foldr insert_*} _ _")
    2.14 -  haskell ("{*foldr insert_*} _ _")
    2.15 +  ml ("{*foldr insert_*}")
    2.16 +  haskell ("{*foldr insert_*}")
    2.17  
    2.18  code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    2.19 -  ml ("{*(flip o foldr) remove*} _ _")
    2.20 -  haskell ("{*(flip o foldr) remove*} _ _")
    2.21 +  ml ("{*(flip o foldr) remove*}")
    2.22 +  haskell ("{*(flip o foldr) remove*}")
    2.23  
    2.24  code_syntax_const "op Int"
    2.25 -  ml ("{*inter*} _ _")
    2.26 -  haskell ("{*inter*} _ _")
    2.27 +  ml ("{*inter*}")
    2.28 +  haskell ("{*inter*}")
    2.29  
    2.30  code_syntax_const "image"
    2.31 -  ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
    2.32 -  haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
    2.33 +  ml ("{*\<lambda>f. foldr (insert_ o f)*}")
    2.34 +  haskell ("{*\<lambda>f. foldr (insert_ o f)*}")
    2.35  
    2.36  code_syntax_const "INTER"
    2.37 -  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
    2.38 -  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
    2.39 +  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
    2.40 +  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
    2.41  
    2.42  code_syntax_const "UNION"
    2.43 -  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
    2.44 -  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
    2.45 +  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
    2.46 +  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
    2.47  
    2.48  code_primconst "Ball"
    2.49  ml {*