--- a/Quot/Examples/AbsRepTest.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -5,7 +5,14 @@
 print_maps
 
 quotient_type 
-  fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  done
+
+quotient_type 
+  'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(auto)
@@ -17,13 +24,11 @@
 Quotient_Info.quotient_rules_get @{context}
 *}
 
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
-  sorry
+quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)"
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  done
 
 print_quotients
 
@@ -32,11 +37,23 @@
 *}
 
 ML {*
-absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"})
+absrep_fun_chk absF @{context} 
+     (@{typ "(('a * 'a) list) list"}, 
+      @{typ "(('a * 'a) fset) fset"})
 |> Syntax.string_of_term @{context}
 |> writeln
 *}
 
+(*
+ML {*
+absrep_fun_chk absF @{context} 
+     (@{typ "('a * 'a) list"}, 
+      @{typ "'a foo"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+*)
+
 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
 term "option_map (map rep_int \<circ> rep_fset)"

--- a/Quot/Examples/FSet.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -23,7 +23,7 @@
   done
 
 quotient_type 
-  fset = "'a list" / "list_eq"
+  'a fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_definition
@@ -280,7 +280,7 @@
 apply (lifting list_induct_part)
 done
 
-quotient_type fset2 = "'a list" / "list_eq"
+quotient_type 'a fset2 = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_definition

--- a/Quot/Examples/FSet2.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -21,7 +21,8 @@
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by (auto intro: list_eq.intros list_eq_refl)
 
-quotient_type fset = "'a list" / "list_eq"
+quotient_type 
+  'a fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_definition

--- a/Quot/Examples/FSet3.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -15,7 +15,7 @@
 (* FIXME-TODO: because of beta-reduction, one cannot give the *)
 (* FIXME-TODO: relation as a term or abbreviation             *) 
 quotient_type 
-  fset = "'a list" / "list_eq"
+  'a fset = "'a list" / "list_eq"
 by (rule list_eq_equivp)
 
 

--- a/Quot/Examples/IntEx.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -7,7 +7,8 @@
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
-quotient_type my_int = "nat \<times> nat" / intrel
+quotient_type 
+  my_int = "nat \<times> nat" / intrel
   apply(unfold equivp_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done

--- 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 "/"