--- a/FSet.thy	Sat Oct 31 11:20:55 2009 +0100
+++ b/FSet.thy	Mon Nov 02 09:39:29 2009 +0100
@@ -44,7 +44,7 @@
 thm EMPTY_def
 
 quotient_def (for "'a fset")
-  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet"
+  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
 
@@ -168,10 +168,10 @@
 thm fold_def
 
 (* FIXME: does not work yet for all types*)
-quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def (for "'a fset" "'b fset")
+  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fmap \<equiv> map"
 
 term map
 term fmap
@@ -296,6 +296,9 @@
  by simp (rule list_eq_refl)
 
 
+print_quotients
+
+
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}

--- a/QuotMain.thy	Sat Oct 31 11:20:55 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 09:39:29 2009 +0100
@@ -159,17 +159,13 @@
 section {* lifting of constants *}
 
 ML {*
-(* whether ty1 is an instance of ty2 *)
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2)
-
 fun lookup_snd _ [] _ = NONE
   | lookup_snd eq ((value, key)::xs) key' =
       if eq (key', key) then SOME value
       else lookup_snd eq xs key';
 
 fun lookup_qenv qenv qty =
-  (case (AList.lookup matches qenv qty) of
+  (case (AList.lookup (op =) qenv qty) of
     SOME rty => SOME (qty, rty)
   | NONE => NONE)
 *}
@@ -225,7 +221,7 @@
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if (AList.defined matches qenv ty)
+  if (AList.defined (op =) qenv ty)
   then (get_const flag (the (lookup_qenv qenv ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
@@ -259,11 +255,10 @@
 end
 *}
 
-ML {* lookup_snd *}
 
 ML {*
 fun exchange_ty qenv ty =
-  case (lookup_snd matches qenv ty) of
+  case (lookup_snd (op =) qenv ty) of
     SOME qty => qty
   | NONE =>
     (case ty of
@@ -272,6 +267,18 @@
     )
 *}
 
+ML {* 
+fun ppair lthy (ty1, ty2) =
+  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+*}
+
+ML {*
+fun print_env qenv lthy =
+  map (ppair lthy) qenv
+  |> commas
+  |> tracing
+*}
+
 ML {*
 fun make_const_def nconst_bname otrm mx qenv lthy =
 let
@@ -279,6 +286,11 @@
   val nconst_ty = exchange_ty qenv otrm_ty
   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst otrm qenv lthy
+
+  val _ = print_env qenv lthy
+  val _ = Syntax.string_of_typ lthy otrm_ty |> tracing
+  val _ = Syntax.string_of_typ lthy nconst_ty |> tracing
+  val _ = Syntax.string_of_term lthy def_trm |> tracing
 in
   define (nconst_bname, mx, def_trm) lthy
 end
@@ -288,46 +300,37 @@
 fun build_qenv lthy qtys = 
 let
   val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-
-  fun find_assoc qty =
-    case (AList.lookup matches qenv qty) of
-      SOME rty => (qty, rty)
-    | NONE => error (implode 
-              ["Quotient type ",     
-               quote (Syntax.string_of_typ lthy qty), 
-               " does not exists"])
+  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
+  
+  fun find_assoc ((qty', rty')::rest) qty =
+        let 
+          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
+        in
+           (Envir.norm_type inst qty, Envir.norm_type inst rty')
+        end
+    | find_assoc [] qty =
+        let 
+          val qtystr =  quote (Syntax.string_of_typ lthy qty)
+        in
+          error (implode ["Quotient type ", qtystr, " does not exists"])
+        end
 in
-  map find_assoc qtys
+  map (find_assoc qenv) qtys
 end
 *}
 
 ML {*
-(* taken from isar_syn.ML *)
-val constdecl =
-  OuterParse.binding --
-    (OuterParse.where_ >> K (NONE, NoSyn) ||
-      OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_) ||
-      Scan.ahead (OuterParse.$$$ "(") |-- 
-      OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))
-*}
-
-ML {*
 val qd_parser = 
   (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
-*}
-
-ML {* 
-fun pair lthy (ty1, ty2) =
-  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
 *}
 
 ML {*
-fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = 
+fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = 
 let
   val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
   val qenv = build_qenv lthy qtys
+  val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
   val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
   val (lhs, rhs) = Logic.dest_equals prop
 in
@@ -340,6 +343,8 @@
   OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
 *}
 
+(* ML {* show_all_types := true *} *)
+
 section {* ATOMIZE *}
 
 text {*

--- a/QuotTest.thy	Sat Oct 31 11:20:55 2009 +0100
+++ b/QuotTest.thy	Mon Nov 02 09:39:29 2009 +0100
@@ -2,6 +2,7 @@
 imports QuotMain
 begin
 
+
 section {* various tests for quotient types*}
 datatype trm =
   var  "nat"

--- a/quotient.ML	Sat Oct 31 11:20:55 2009 +0100
+++ b/quotient.ML	Mon Nov 02 09:39:29 2009 +0100
@@ -6,7 +6,7 @@
   val mk_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
-  val maps_lookup: theory -> string -> maps_info option
+  val maps_lookup_thy: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
@@ -32,7 +32,9 @@
    val extend = I
    fun merge _ = Symtab.merge (K true))
 
-val maps_lookup = Symtab.lookup o MapsData.get
+val maps_lookup_thy = Symtab.lookup o MapsData.get
+
+
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
 
@@ -242,7 +244,7 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))