--- a/quotient.ML	Fri Nov 06 11:01:22 2009 +0100
+++ b/quotient.ML	Fri Nov 06 11:02:11 2009 +0100
@@ -2,7 +2,7 @@
 sig
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
-  val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
+
   val note: binding * thm -> local_theory -> thm * local_theory
 end;
 
@@ -212,8 +212,8 @@
   fun parse_spec (((qty_str, mx), rty_str), rel_str) =
   let
     val qty_name = Binding.name qty_str
-    val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy
-    val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy
+    val rty = Syntax.read_typ lthy rty_str
+    val rel = Syntax.read_term lthy rel_str 
   in
     ((qty_name, mx), (rty, rel))
   end