--- a/quotient.ML	Mon Oct 12 23:16:20 2009 +0200
+++ b/quotient.ML	Mon Oct 12 23:39:14 2009 +0200
@@ -163,10 +163,8 @@
 (* syntax setup *)
 local structure P = OuterParse in
 
-fun mk_typedef (qty, mx, rty, rel_trm) lthy = 
+fun mk_typedef (qty_name, mx, rty, rel_trm) lthy = 
 let
-  val (qty_name, _) = Term.dest_Type qty 
-
   val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
 		    
@@ -181,18 +179,17 @@
 end
 
 val quottype_parser = 
-    P.typ -- P.opt_infix -- 
+    P.short_ident -- P.opt_infix -- 
        (P.$$$ "=" |-- P.typ) -- 
          (P.$$$ "/" |-- P.term)
            
 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = 
 let
-  val qty = Syntax.parse_typ lthy qstr
   val rty = Syntax.parse_typ lthy rstr
   val rel_trm = Syntax.parse_term lthy rel_str
                 |> Syntax.check_term lthy
 in
-  mk_typedef (qty, mx, rty, rel_trm) lthy  
+  mk_typedef (qstr, mx, rty, rel_trm) lthy  
 end
 
 val _ = OuterKeyword.keyword "/"