--- a/QuotMain.thy	Tue Nov 03 17:30:27 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -140,8 +140,15 @@
 
 section {* type definition for the quotient type *}
 
+(* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
-use "quotient.ML"
+
+ML {*
+fun error_msg pre post msg = 
+  msg |> quote
+      |> enclose (pre ^ " ") (" " ^ post) 
+      |> error  
+*}
 
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
@@ -151,6 +158,11 @@
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 
+
+(* definition of the quotient types *)
+use "quotient.ML"
+
+
 text {* FIXME: auxiliary function *}
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -238,7 +250,6 @@
 end
 *}
 
-
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -290,65 +301,56 @@
   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
 *}
 
 ML {*
-fun build_qenv lthy qtys = 
-let
-  val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-  val thy = ProofContext.theory_of lthy
-  
-  fun find_assoc ((qty', rty')::rest) qty =
-        let 
-          val inst = Sign.typ_match thy (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 qenv) qtys
-end
+(* difference of two types *)
+fun diff (T, S) Ds =
+  case (T, S) of
+    (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
+  | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
+  | (Type (a, Ts), Type (b, Us)) => 
+      if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
+  | _ => (T, S)::Ds
+and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
+  | diffs ([], []) Ds = Ds
+  | diffs _ _ = error "Unequal length of type arguments"
 *}
 
-
 ML {*
-fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy =
+fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy =
 let    
-  val (lhs_, rhs) = Logic.dest_equals prop
+  val (_, rhs) = Logic.dest_equals prop
+  val rty = fastype_of rhs
+  val qenv = distinct (op=) (diff (qty, rty) [])
 in
   make_const_def bind rhs mx qenv lthy
 end
 *}
 
 ML {*
-val quotdef_parser = 
-  Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- 
-       OuterParse.prop)) >> OuterParse.triple2
+val constdecl =
+  OuterParse.binding --
+    (OuterParse.$$$ "::" |-- OuterParse.!!! 
+      (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_))
+  >> OuterParse.triple2;
 *}
 
 ML {*
-fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = 
+val quotdef_parser = 
+  (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) 
+*}
+
+ML {*
+fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy = 
 let
-  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs)
-  val qenv = build_qenv lthy qtys
-  val qty  = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr
-  val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
+  val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
+  val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
 in
-  quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd
+  quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 *}