# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265988445 -3600
# Node ID 3c8ad149a4d3f7a6461c5aaa8ac8a94192e974d2
# Parent  aaeb5a34d21a336c66331a6c1599498951ef69b8
Undid the read_terms change; now compiles.

diff -r aaeb5a34d21a -r 3c8ad149a4d3 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Feb 12 16:06:09 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Feb 12 16:27:25 2010 +0100
@@ -33,11 +33,11 @@
 
 quotient_definition
   "fempty :: 'a fset" ("{||}")
-as "[]::'a list"
+is "[]::'a list"
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
-as "op #"
+is "op #"
 
 syntax
   "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
@@ -53,7 +53,7 @@
 
 quotient_definition
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
-as "memb"
+is "memb"
 
 abbreviation
   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
@@ -149,7 +149,7 @@
 
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
-as "fcard_raw"
+is "fcard_raw"
 
 text {* raw section *}
 
diff -r aaeb5a34d21a -r 3c8ad149a4d3 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Feb 12 16:06:09 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Feb 12 16:27:25 2010 +0100
@@ -71,7 +71,8 @@
 
 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
 let
-  val [lhs, rhs] = Syntax.read_terms lthy [lhs_str, rhs_str]
+  val lhs = Syntax.read_term lthy lhs_str
+  val rhs = Syntax.read_term lthy rhs_str
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in