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*}")