diff -r d6407afb913c -r 5cf83fa5b36c Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/quotient_typ.ML	Thu Dec 24 22:28:19 2009 +0100
@@ -2,9 +2,10 @@
 sig
   exception LIFT_MATCH of string
 
-  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 quotient_type: ((string list * binding * mixfix) * (typ * term)) list 
+    -> Proof.context -> Proof.state
+  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list 
+    -> Proof.context -> Proof.state
 end;
 
 structure Quotient_Type: QUOTIENT_TYPE =
@@ -60,18 +61,17 @@
 end
 
 (* makes the new type definitions and proves non-emptyness*)
-fun typedef_make (qty_name, mx, rel, rty) lthy =
+fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
      EVERY1 [rtac @{thm exI},
              rtac mem_def2, 
              rtac @{thm exI},
              rtac @{thm refl}]
-  val tfrees = map fst (Term.add_tfreesT rty [])
 in
   Local_Theory.theory_result
     (Typedef.add_typedef false NONE
-       (qty_name, tfrees, mx)
+       (qty_name, vs, mx)
          (typedef_term rel rty lthy)
            NONE typedef_tac) lthy
 end
@@ -120,10 +120,10 @@
 end
 
 (* main function for constructing a quotient type *)
-fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
+fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
   (* generates the typedef *)
-  val ((qty_full_name, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
+  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
 
   (* abs and rep functions from the typedef *)
   val Abs_ty = #abs_type typedef_info
@@ -196,13 +196,12 @@
            
 fun quotient_type_cmd spec lthy = 
 let
-  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
+  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =
   let
-    val qty_name = Binding.name qty_str
     val rty = Syntax.read_typ lthy rty_str
     val rel = Syntax.read_term lthy rel_str 
   in
-    ((qty_name, mx), (rty, rel))
+    ((vs, qty_name, mx), (rty, rel))
   end
 in
   quotient_type (map parse_spec spec) lthy
@@ -210,8 +209,8 @@
 
 val quotspec_parser = 
     OuterParse.and_list1
-     (OuterParse.short_ident -- OuterParse.opt_infix -- 
-       (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
+     ((OuterParse.type_args -- OuterParse.binding) -- 
+        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
          (OuterParse.$$$ "/" |-- OuterParse.term))
 
 val _ = OuterKeyword.keyword "/"