--- a/FSet.thy	Wed Oct 28 14:59:24 2009 +0100
+++ b/FSet.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -36,7 +36,7 @@
 
 ML {* @{term "Abs_fset"} *}
 local_setup {*
-  make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Nil
@@ -45,7 +45,7 @@
 
 
 local_setup {*
-  make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term Cons
@@ -53,7 +53,7 @@
 thm INSERT_def
 
 local_setup {*
-  make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term append
@@ -78,7 +78,7 @@
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
 local_setup {*
-  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term card1
@@ -143,7 +143,7 @@
   done
 
 local_setup {*
-  make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term membship
@@ -151,7 +151,7 @@
 thm IN_def
 
 local_setup {*
-  make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term fold1
@@ -159,7 +159,7 @@
 thm fold_def
 
 local_setup {*
-  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
+  old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
   @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 

--- a/IntEx.thy	Wed Oct 28 14:59:24 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -12,27 +12,17 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-print_quotients
-
-typ my_int
+quotient_def (for my_int)
+  ZERO::"my_int"
+where
+  "ZERO \<equiv> (0::nat, 0::nat)"
 
-local_setup {*
-  make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
-
-term ZERO
 thm ZERO_def
 
-(*
-quotient_def (with my_int)
-  ZERO :: "my_int"
+quotient_def (for my_int)
+  ONE::"my_int"
 where
-  "ZERO \<equiv> (0::nat, 0::nat)"
-*)
-
-local_setup {*
-  make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+  "ONE \<equiv> (1::nat, 0::nat)"
 
 term ONE
 thm ONE_def
@@ -42,9 +32,10 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-local_setup {*
-  make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+quotient_def (for my_int)
+  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+  "PLUS \<equiv> my_plus"
 
 term PLUS
 thm PLUS_def
@@ -55,7 +46,7 @@
   "my_neg (x, y) = (y, x)"
 
 local_setup {*
-  make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term NEG
@@ -72,7 +63,7 @@
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 local_setup {*
-  make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term MULT
@@ -85,7 +76,7 @@
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
 local_setup {*
-  make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term LE

--- a/LamEx.thy	Wed Oct 28 14:59:24 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -23,11 +23,15 @@
 print_quotients
 
 local_setup {*
-  make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
+  old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
 *}
 
+thm Var_def
+thm App_def
+thm Lam_def
+
 lemma real_alpha:
   assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
   shows "Lam a t = Lam b s"

--- a/QuotMain.thy	Wed Oct 28 14:59:24 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -147,32 +147,7 @@
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 
-ML {*
-fun matches ty1 ty2 =
-  Type.raw_instance (ty1, Logic.varifyT ty2)
-*}
-
-
-
-ML {*
-val quot_def_parser = 
-  (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
-    ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
-      (OuterParse.binding -- 
-        Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- 
-         OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)
-*}
-
-ML {*
-fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy
-*}
-
-ML {*
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (quot_def_parser >> test)
-*}
-
-(* FIXME: auxiliary function *)
+text {* FIXME: auxiliary function *}
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
@@ -184,7 +159,19 @@
 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
+    SOME rty => SOME (qty, rty)
+  | NONE => NONE)
 *}
 
 ML {*
@@ -198,10 +185,9 @@
 fun negF absF = repF
   | negF repF = absF
 
-fun get_fun flag rty qty lthy ty =
+fun get_fun flag qenv lthy ty =
 let
-  val qty_name = Long_Name.base_name (fst (dest_Type qty))
-
+  
   fun get_fun_aux s fs_tys =
   let
     val (fs, tys) = split_list fs_tys
@@ -226,22 +212,27 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
-  val thy = ProofContext.theory_of lthy
-
-  fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
-    | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+  fun get_const flag (qty, rty) =
+  let 
+    val thy = ProofContext.theory_of lthy
+    val qty_name = Long_Name.base_name (fst (dest_Type qty))
+  in
+    case flag of
+      absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
+    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+  end
 
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if ty = qty
-  then (get_const flag)
+  if (AList.defined matches qenv ty)
+  then (get_const flag (the (lookup_qenv qenv ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty)) 
         | Type ("fun" , [ty1, ty2]) => 
-                 get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
-        | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
+                 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
+        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
         | _ => raise ERROR ("no type variables")
        )
 end
@@ -251,50 +242,104 @@
 text {* produces the definition for a lifted constant *}
 
 ML {*
-fun get_const_def nconst oconst rty qty lthy =
+fun get_const_def nconst otrm qenv lthy =
 let
   val ty = fastype_of nconst
   val (arg_tys, res_ty) = strip_type ty
 
-  val fresh_args = arg_tys |> map (pair "x")
-                           |> Variable.variant_frees lthy [nconst, oconst]
-                           |> map Free
-
-  val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
-  val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty
+  val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
+  val abs_fn  = (fst o get_fun absF qenv lthy) res_ty
 
   fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
 
-  val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
+  val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)
             |> Syntax.check_term lthy
 in
-  fns $ oconst
+  fns $ otrm
 end
 *}
 
+ML {* lookup_snd *}
+
 ML {*
-fun exchange_ty rty qty ty =
-  if ty = rty
-  then qty
-  else
+fun exchange_ty qenv ty =
+  case (lookup_snd matches qenv ty) of
+    SOME qty => qty
+  | NONE =>
     (case ty of
-       Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
+       Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
       | _ => ty
     )
 *}
 
 ML {*
-fun make_const_def nconst_bname oconst mx rty qty lthy =
+fun make_const_def nconst_bname otrm mx qenv lthy =
 let
-  val oconst_ty = fastype_of oconst
-  val nconst_ty = exchange_ty rty qty oconst_ty
+  val otrm_ty = fastype_of otrm
+  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 oconst rty qty lthy
+  val def_trm = get_const_def nconst otrm qenv lthy
 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)
+
+  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"])
+in
+  map find_assoc 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) ^ ")"
+*}
+
+ML {*
+fun parse_qd_spec (qtystrs, ((bind, (typstr__, 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 prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
+  val (lhs, rhs) = Logic.dest_equals prop
+in
+  make_const_def bind rhs mx qenv lthy |> snd
+end
+*}
+
+ML {*
+val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
+  OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
+*}
+
 section {* ATOMIZE *}
 
 text {*
@@ -587,17 +632,36 @@
 by (simp add: id_def)
 
 ML {*
+fun old_exchange_ty rty qty ty =
+  if ty = rty
+  then qty
+  else
+     (case ty of
+        Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
+      | _ => ty
+     )
+*}
+
+ML {*
+fun old_get_fun flag rty qty lthy ty =
+  get_fun flag [(qty, rty)] lthy ty 
+
+fun old_make_const_def nconst_bname otrm mx rty qty lthy =
+  make_const_def nconst_bname otrm mx [(qty, rty)] lthy
+*}
+
+ML {*
 fun build_repabs_term lthy thm constructors rty qty =
   let
     fun mk_rep tm =
       let
-        val ty = exchange_ty rty qty (fastype_of tm)
-      in fst (get_fun repF rty qty lthy ty) $ tm end
+        val ty = old_exchange_ty rty qty (fastype_of tm)
+      in fst (old_get_fun repF rty qty lthy ty) $ tm end
 
     fun mk_abs tm =
       let
-        val ty = exchange_ty rty qty (fastype_of tm) in
-      fst (get_fun absF rty qty lthy ty) $ tm end
+        val ty = old_exchange_ty rty qty (fastype_of tm) in
+      fst (old_get_fun absF rty qty lthy ty) $ tm end
 
     fun is_constructor (Const (x, _)) = member (op =) constructors x
       | is_constructor _ = false;

--- a/quotient.ML	Wed Oct 28 14:59:24 2009 +0100
+++ b/quotient.ML	Wed Oct 28 15:25:36 2009 +0100
@@ -10,7 +10,8 @@
   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
-  val quotdata_lookup: theory -> quotient_info list
+  val quotdata_lookup_thy: theory -> quotient_info list
+  val quotdata_lookup: Proof.context -> quotient_info list
   val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
 end;
@@ -70,7 +71,8 @@
    val extend = I
    fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
 
-val quotdata_lookup = QuotData.get
+val quotdata_lookup_thy = QuotData.get
+val quotdata_lookup = QuotData.get o ProofContext.theory_of
 
 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
       QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy