# HG changeset patch
# User haftmann
# Date 1140877159 -3600
# Node ID f92919b141b2ead08e2d9763337d38ec266a5d3d
# Parent  00ade10f611dc5bcfe9b207bdb30f67989762fdb
change in codegen syntax

diff -r 00ade10f611d -r f92919b141b2 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Sat Feb 25 15:19:00 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Sat Feb 25 15:19:19 2006 +0100
@@ -63,7 +63,7 @@
   ml (target_atom "IntInf.int")
   haskell (target_atom "Integer")
 
-code_syntax_const 0 :: nat
+code_syntax_const "0 :: nat"
   ml (target_atom "(0:IntInf.int)")
   haskell (target_atom "0")
 
diff -r 00ade10f611d -r f92919b141b2 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Sat Feb 25 15:19:00 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Sat Feb 25 15:19:19 2006 +0100
@@ -95,28 +95,28 @@
   Fract
     ml ("{*of_quotient*}")
     haskell ("{*of_quotient*}")
-  0 :: "rat"
+  "0 :: rat"
     ml ("{*0::erat*}")
     haskell ("{*1::erat*}")
-  1 :: "rat"
+  "1 :: rat"
     ml ("{*1::erat*}")
     haskell ("{*1::erat*}")
-  "op +" :: "rat \<Rightarrow> rat \<Rightarrow> rat"
+  "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
     ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
     haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  uminus :: "rat \<Rightarrow> rat"
+  "uminus :: rat \<Rightarrow> rat"
     ml ("{*uminus :: erat \<Rightarrow> erat*}")
     haskell ("{*uminus :: erat \<Rightarrow> erat*}")
-  "op *" :: "rat \<Rightarrow> rat \<Rightarrow> rat"
+  "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
     ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
     haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  inverse :: "rat \<Rightarrow> rat"
+  "inverse :: rat \<Rightarrow> rat"
     ml ("{*inverse :: erat \<Rightarrow> erat*}")
     haskell ("{*inverse :: erat \<Rightarrow> erat*}")
-  divide :: "rat \<Rightarrow> rat \<Rightarrow> rat"
+  "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
     ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
     haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
-  "op <=" :: "rat \<Rightarrow> rat \<Rightarrow> bool"
+  "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
     ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
     haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
 
diff -r 00ade10f611d -r f92919b141b2 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Sat Feb 25 15:19:00 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Sat Feb 25 15:19:19 2006 +0100
@@ -82,7 +82,7 @@
   "inter [] ys = []"
   "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
 
-code_syntax_const "insert"
+code_syntax_const insert
   ml ("{*insert_*}")
   haskell ("{*insert_*}")
 
@@ -90,7 +90,7 @@
   ml ("{*foldr insert_*}")
   haskell ("{*foldr insert_*}")
 
-code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+code_syntax_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
   ml ("{*(flip o foldr) remove*}")
   haskell ("{*(flip o foldr) remove*}")
 
@@ -98,19 +98,19 @@
   ml ("{*inter*}")
   haskell ("{*inter*}")
 
-code_syntax_const "image"
+code_syntax_const image
   ml ("{*\<lambda>f. foldr (insert_ o f)*}")
   haskell ("{*\<lambda>f. foldr (insert_ o f)*}")
 
-code_syntax_const "INTER"
+code_syntax_const INTER
   ml ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
   haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
 
-code_syntax_const "UNION"
+code_syntax_const UNION
   ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
   haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
 
-code_primconst "Ball"
+code_primconst Ball
 ml {*
 fun `_` [] f = true
   | `_` (x::xs) f = f x andalso `_` xs f;
@@ -119,7 +119,7 @@
 `_` = flip all
 *}
 
-code_primconst "Bex"
+code_primconst Bex
 ml {*
 fun `_` [] f = false
   | `_` (x::xs) f = f x orelse `_` xs f;