--- a/IntEx.thy	Fri Nov 20 13:03:01 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 02:49:39 2009 +0100
@@ -8,10 +8,13 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
+  and    my_int' = "nat \<times> nat" / intrel
   apply(unfold EQUIV_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+thm my_int_equiv
+
 print_theorems
 print_quotients
 
@@ -98,6 +101,7 @@
 term LE
 thm LE_def
 
+
 definition
   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
@@ -149,12 +153,33 @@
   val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
 *}
 
-
 ML {*
-  val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
-  val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) 
+  val aqtrm = (prop_of (atomize_thm test))
+  val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) 
+  val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm
 *}
 
+prove {* reg_artm  *}
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
+done
+
+(*
+ML {*
+fun inj_REPABS lthy rtrm qtrm =
+  case (rtrm, qtrm) of
+    (Abs (x, T, t), Abs (x', T', t')) =>
+    if T = T'
+    then Abs (x, T, inj_REPABS lthy t t')
+    else 
+      let 
+         
+      in
+
+      end
+  | _ => rtrm
+*}
+*)
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -164,8 +189,17 @@
   apply (simp)
   done
 
-ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
+ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
+ML {*
+  val aqtrm = (prop_of (atomize_thm test2))
+  val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) 
+*}
+
+prove {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
+done
 
 
 

--- a/QuotMain.thy	Fri Nov 20 13:03:01 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 02:49:39 2009 +0100
@@ -557,7 +557,62 @@
 *}
 
 ML {*
-fun get_fun_new flag (rty, qty) lthy ty =
+fun negF absF = repF
+  | negF repF = absF
+
+fun get_fun flag qenv lthy ty =
+let
+  
+  fun get_fun_aux s fs =
+   (case (maps_lookup (ProofContext.theory_of lthy) s) of
+      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+    | NONE      => error ("no map association for type " ^ s))
+
+  fun get_const flag qty =
+  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), dummyT)
+    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+  end
+
+  fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+  if (AList.defined (op=) qenv ty)
+  then (get_const flag ty)
+  else (case ty of
+          TFree _ => mk_identity ty
+        | Type (_, []) => mk_identity ty 
+        | Type ("fun" , [ty1, ty2]) => 
+            let
+              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+              val fs_ty2 = get_fun flag qenv lthy ty2
+            in  
+              get_fun_aux "fun" [fs_ty1, fs_ty2]
+            end 
+        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
+        | _ => error ("no type variables allowed"))
+end
+
+(* returns all subterms where two types differ *)
+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 get_fun_OLD flag (rty, qty) lthy ty =
   let
     val tys = find_matching_types rty ty;
     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
@@ -657,11 +712,11 @@
   fun mk_abs tm =
     let
       val ty = fastype_of tm
-    in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+    in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
   fun mk_repabs tm =
     let
       val ty = fastype_of tm
-    in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
+    in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
 
     fun is_lifted_const (Const (x, _)) = member (op =) consts x
       | is_lifted_const _ = false;
@@ -1008,11 +1063,11 @@
     fun mk_rep tm =
       let
         val ty = exchange_ty lthy qty rty (fastype_of tm)
-      in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end;
+      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
     fun mk_abs tm =
       let
         val ty = fastype_of tm
-      in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+      in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
     val (l, ltl) = Term.strip_type ty;
     val nl = map absty l;
     val vs = map (fn _ => "x") l;
@@ -1149,7 +1204,6 @@
 (******************************************)
 
 (* exception for when qtrm and rtrm do not match *)
-ML {* exception LIFT_MATCH of string *}
 
 ML {*
 fun mk_resp_arg lthy (rty, qty) =
@@ -1161,7 +1215,7 @@
        if s = s' 
        then let
               val SOME map_info = maps_lookup thy s
-              val args = map (mk_resp_arg lthy) (tys ~~tys')
+              val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
               list_comb (Const (#relfun map_info, dummyT), args) 
             end  
@@ -1192,12 +1246,28 @@
 fun qnt_typ ty = domain_type (domain_type ty)
 *}
 
+(*
+Regularizing an rterm means:
+ - Quantifiers over a type that needs lifting are replaced by
+   bounded quantifiers, for example:
+      \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
+ - Abstractions over a type that needs lifting are replaced
+   by bounded abstractions:
+      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
+
+ - Equalities over the type being lifted are replaced by
+   appropriate relations:
+      A = B     \<Longrightarrow>     A \<approx> B
+   Example with more complicated types of A, B:
+      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
+*)
+
 ML {*
-fun REGULARIZE_aux lthy rtrm qtrm =
+fun REGULARIZE_trm lthy rtrm qtrm =
   case (rtrm, qtrm) of
     (Abs (x, T, t), Abs (x', T', t')) =>
        let
-         val subtrm = REGULARIZE_aux lthy t t'
+         val subtrm = REGULARIZE_trm lthy t t'
        in     
          if T = T'
          then Abs (x, T, subtrm)
@@ -1205,7 +1275,7 @@
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -1213,7 +1283,7 @@
        end
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "Ex"}, ty) $ subtrm
@@ -1222,14 +1292,14 @@
   (* FIXME: why is there a case for equality? is it correct? *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
-         val subtrm = REGULARIZE_aux lthy t t'
+         val subtrm = REGULARIZE_trm lthy t t'
        in
          if ty = ty'
          then Const (@{const_name "op ="}, ty) $ subtrm
          else mk_resp_arg lthy (ty, ty') $ subtrm
        end 
   | (t1 $ t2, t1' $ t2') =>
-       (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2')
+       (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
        then rtrm 
@@ -1246,11 +1316,98 @@
 *}
 
 ML {*
-fun REGULARIZE_trm lthy rtrm qtrm =
-  REGULARIZE_aux lthy rtrm qtrm
-  |> Syntax.check_term lthy
-  
+fun mk_REGULARIZE_goal lthy rtrm qtrm =
+      Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
 *}
 
+(*
+To prove that the old theorem implies the new one, we first
+atomize it and then try:
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
+
+lemma my_equiv_res_forall2:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes a: "(All Q) \<longrightarrow> (All P)"
+  shows "(All Q) \<longrightarrow> Ball (Respects E) P"
+using a by auto
+
+lemma my_equiv_res_exists:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  and     b: "(Ex Q) \<longrightarrow> (Ex P)"
+  shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
+apply(subst equiv_res_exists)
+apply(rule a)
+apply(rule b)
+done
+
+ML {*
+fun REGULARIZE_tac lthy rel_refl rel_eqv =
+  ObjectLogic.full_atomize_tac THEN'
+   REPEAT_ALL_NEW (FIRST' 
+     [rtac rel_refl,
+      atac,
+      rtac @{thm universal_twice},
+      rtac @{thm impI} THEN' atac,
+      rtac @{thm implication_twice},
+      rtac @{thm my_equiv_res_forall2},
+      rtac (rel_eqv RS @{thm my_equiv_res_exists}),
+      (* For a = b \<longrightarrow> a \<approx> b *)
+      rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
+      rtac @{thm RIGHT_RES_FORALL_REGULAR}])
+*}
+
+(* same version including debugging information *)
+ML {*
+fun my_print_tac ctxt s thm =
+let
+  val prems_str = prems_of thm
+                  |> map (Syntax.string_of_term ctxt)
+                  |> cat_lines
+  val _ = tracing (s ^ "\n" ^ prems_str)
+in
+  Seq.single thm
+end
+ 
+fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+*}
+
+ML {*
+fun REGULARIZE_tac' lthy rel_refl rel_eqv =
+   (REPEAT1 o FIRST1) 
+     [(K (print_tac "start")) THEN' (K no_tac), 
+      DT lthy "1" (rtac rel_refl),
+      DT lthy "2" atac,
+      DT lthy "3" (rtac @{thm universal_twice}),
+      DT lthy "4" (rtac @{thm impI} THEN' atac),
+      DT lthy "5" (rtac @{thm implication_twice}),
+      DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
+      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
+      (* For a = b \<longrightarrow> a \<approx> b *)
+      DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+      DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
+*}
+
+ML {*
+fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
+  let
+    val goal = mk_REGULARIZE_goal lthy rtrm qtrm
+    val cthm = Goal.prove lthy [] [] goal 
+      (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1)
+  in
+    cthm 
+  end
+*}
+
+
 end
 

--- a/quotient.ML	Fri Nov 20 13:03:01 2009 +0100
+++ b/quotient.ML	Sat Nov 21 02:49:39 2009 +0100
@@ -1,5 +1,7 @@
 signature QUOTIENT =
 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
 
@@ -9,6 +11,9 @@
 structure Quotient: QUOTIENT =
 struct
 
+(* exception for when quotient and lifted things do not match *)
+exception LIFT_MATCH of string 
+
 (* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
@@ -150,15 +155,17 @@
   val _ = tracing ("storing under: " ^ qty_str)
   val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
+  (* storing of the equiv_thm under a name *)
+  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
-  val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3;
+  val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
   val eqn1i = Thm.prop_of (symmetric eqn1pre)
-  val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4;
+  val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
   val eqn2i = Thm.prop_of (symmetric eqn2pre)
 
-  val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5));
+  val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
   val exp_term = Morphism.term exp_morphism;
   val exp = Morphism.thm exp_morphism;
 
@@ -169,14 +176,14 @@
   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
-  lthy5
+  lthy6
   |> note (quot_thm_name, quot_thm)
   ||>> note (quotient_thm_name, quotient_thm)
   ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
         (* Not sure if the following context should not be used *)
-        val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5;
+        val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end

--- a/quotient_def.ML	Fri Nov 20 13:03:01 2009 +0100
+++ b/quotient_def.ML	Sat Nov 21 02:49:39 2009 +0100
@@ -2,7 +2,7 @@
 signature QUOTIENT_DEF =
 sig
   datatype flag = absF | repF
-  val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term
+  val get_fun: flag -> Proof.context -> typ * typ -> term
   val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
     Proof.context -> (term * thm) * local_theory
 
@@ -10,7 +10,6 @@
     local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
     local_theory -> local_theory
-  val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -25,7 +24,6 @@
   ((rhs, thm), lthy')
 end
 
-
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
    function types need to be treated specially, since repF and absF
@@ -36,99 +34,65 @@
 fun negF absF = repF
   | negF repF = absF
 
-fun get_fun flag qenv lthy ty =
-let
-  
-  fun get_fun_aux s fs =
-   (case (maps_lookup (ProofContext.theory_of lthy) s) of
-      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-    | NONE      => error ("no map association for type " ^ s))
-
-  fun get_const flag qty =
-  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), dummyT)
-    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
-  end
+fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-  fun mk_identity ty = Abs ("", ty, Bound 0)
-
+fun ty_lift_error lthy rty qty =
+let
+  val rty_str = quote (Syntax.string_of_typ lthy rty) 
+  val qty_str = quote (Syntax.string_of_typ lthy qty)
+  val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."]
 in
-  if (AList.defined (op=) qenv ty)
-  then (get_const flag ty)
-  else (case ty of
-          TFree _ => mk_identity ty
-        | Type (_, []) => mk_identity ty 
-        | Type ("fun" , [ty1, ty2]) => 
-            let
-              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
-              val fs_ty2 = get_fun flag qenv lthy ty2
-            in  
-              get_fun_aux "fun" [fs_ty1, fs_ty2]
-            end 
-        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
-        | _ => error ("no type variables allowed"))
+  raise LIFT_MATCH (space_implode " " msg)
 end
 
-(* returns all subterms where two types differ *)
-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"
+fun get_fun_aux lthy s fs =
+  case (maps_lookup (ProofContext.theory_of lthy) s) of
+    SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+  | NONE      => raise LIFT_MATCH ("no map association for type " ^ s)
 
-
-(* sanity check that the calculated quotient environment
-   matches with the stored quotient environment. *)
-fun sanity_chk qenv lthy =
-let
-  val global_qenv = Quotient_Info.mk_qenv lthy
+fun get_const flag lthy _ qty =
+(* FIXME: check here that _ and qty are related *)
+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), dummyT)
+  | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+end
 
-  fun error_msg lthy (qty, rty) =
-  let 
-    val qtystr = quote (Syntax.string_of_typ lthy qty)
-    val rtystr = quote (Syntax.string_of_typ lthy rty)
-  in
-    error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
-  end
-
-  fun is_inst (qty, rty) (qty', rty') =
-    if Sign.typ_instance thy (qty, qty')
-    then let
-           val inst = Sign.typ_match thy (qty', qty) Vartab.empty
-         in
-           rty = Envir.subst_type inst rty'       
-         end
-    else false
-
-  fun chk_inst (qty, rty) = 
-    if exists (is_inst (qty, rty)) global_qenv 
-    then true
-    else error_msg lthy (qty, rty)
-in
-  map chk_inst qenv
-end
+fun get_fun flag lthy (rty, qty) =
+  case (rty, qty) of 
+    (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+     let
+       val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
+       val fs_ty2 = get_fun flag lthy (ty2, ty2')
+     in  
+       get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
+     end 
+  | (Type (s, []), Type (s', [])) =>
+     if s = s'
+     then mk_identity qty 
+     else get_const flag lthy rty qty
+  | (Type (s, tys), Type (s', tys')) =>
+     if s = s'
+     then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
+     else get_const flag lthy rty qty
+  | (TFree x, TFree x') =>
+     if x = x'
+     then mk_identity qty 
+     else ty_lift_error lthy rty qty
+  | (TVar _, TVar _) => raise LIFT_MATCH "no type variables allowed"
+  | _ => ty_lift_error lthy rty qty
 
 fun make_def nconst_bname qty mx attr rhs lthy =
 let
-  val (arg_tys, res_ty) = strip_type qty
-
   val rty = fastype_of rhs
-  val qenv = distinct (op=) (diff (qty, rty) [])   
-
-  val _ = sanity_chk qenv lthy
-
-  val rep_fns = map (get_fun repF qenv lthy) arg_tys
-  val abs_fn  = (get_fun absF qenv lthy) res_ty
+  val (arg_rtys, res_rty) = strip_type rty
+  val (arg_qtys, res_qty) = strip_type qty
+  
+  val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys)
+  val abs_fn  = get_fun absF lthy (res_rty, res_qty)
 
   fun mk_fun_map t s =  
         Const (@{const_name "fun_map"}, dummyT) $ t $ s
@@ -139,10 +103,9 @@
   val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
 
   val nconst_str = Binding.name_of nconst_bname
-  val qcinfo = {qconst = trm, rconst = rhs}
+  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
   val lthy'' = Local_Theory.declaration true
-                (fn phi => qconsts_update_generic nconst_str 
-                             (qconsts_transfer phi qcinfo)) lthy'
+                 (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
@@ -186,3 +149,5 @@
 end; (* structure *)
 
 open Quotient_Def;
+
+

--- a/quotient_info.ML	Fri Nov 20 13:03:01 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 02:49:39 2009 +0100
@@ -20,7 +20,7 @@
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
-  val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic 
+  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
 end;
 
@@ -147,7 +147,7 @@
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_generic k qcinfo = 
+fun qconsts_update_gen k qcinfo = 
       Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =