--- a/QuotMain.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 13:36:46 2009 +0100
@@ -239,11 +239,8 @@
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
 ML {*
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2);
-
 fun tyRel ty rty rel lthy =
-  if matches (rty, ty)
+  if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
   then rel
   else (case ty of
           Type (s, tys) =>
@@ -260,6 +257,8 @@
         | _ => HOLogic.eq_const ty)
 *}
 
+(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)
+
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
@@ -407,26 +406,39 @@
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 by (simp add: id_def)
 
+(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 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
-     )
+fun exchange_ty lthy rty qty ty =
+  let
+    val thy = ProofContext.theory_of lthy
+  in
+    if Sign.typ_instance thy (ty, rty) then
+      let
+        val inst = Sign.typ_match thy (rty, ty) Vartab.empty
+      in
+        Envir.subst_type inst qty
+      end
+    else
+      let
+        val (s, tys) = dest_Type ty
+      in
+        Type (s, map (exchange_ty lthy rty qty) tys)
+      end
+  end
+  handle _ => ty (* for dest_Type *)
 *}
 
-(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
-ML {* fun exchange_ty rty (qty as (Type (qtys, _))) ty =
-  let val (s, tys) = dest_Type ty in
-    if Type.raw_instance (Logic.varifyT ty, rty)
-    then Type (qtys, tys)
-    else Type (s, map (exchange_ty rty qty) tys)
-  end
-  handle _ => ty
+(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+axioms Rl_eq: "EQUIV Rl"
+
+quotient ql = "'a list" / "Rl"
+  by (rule Rl_eq)
+ML {* 
+  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
+  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
 *}
+*)
+
 
 ML {*
 fun negF absF = repF
@@ -458,9 +470,10 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
+  val thy = ProofContext.theory_of lthy
+
   fun get_const flag (rty, qty) =
   let 
-    val thy = ProofContext.theory_of lthy
     val qty_name = Long_Name.base_name (fst (dest_Type qty))
   in
     case flag of
@@ -471,8 +484,8 @@
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if (Type.raw_instance (Logic.varifyT ty, rty))
-  then (get_const flag (ty, (exchange_ty rty qty ty)))
+  if (Sign.typ_instance thy (ty, rty))
+  then (get_const flag (ty, (exchange_ty lthy rty qty ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty)) 
@@ -501,8 +514,8 @@
 fun get_fun_new flag rty qty lthy ty =
   let
     val tys = find_matching_types rty ty;
-    val qenv = map (fn t => (exchange_ty rty qty t, t)) tys;
-    val xchg_ty = exchange_ty rty qty ty
+    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
+    val xchg_ty = exchange_ty lthy rty qty ty
   in
     get_fun flag qenv lthy xchg_ty
   end
@@ -875,13 +888,14 @@
     | _ => ([], []);
 *}
 ML {*
-  fun findallex rty qty tm =
+  fun findallex lthy rty qty tm =
     let
       val (a, e) = findallex_all rty qty tm;
       val (ad, ed) = (map domain_type a, map domain_type e);
-      val (au, eu) = (distinct (op =) ad, distinct (op =) ed)
+      val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
+      val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
     in
-      (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)
+      (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
     end
 *}
 
@@ -912,10 +926,10 @@
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
   fun absty ty =
-    exchange_ty rty qty ty
+    exchange_ty lthy rty qty ty
   fun mk_rep tm =
     let
-      val ty = exchange_ty qty rty (fastype_of tm)
+      val ty = exchange_ty lthy qty rty (fastype_of tm)
     in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end;
   fun mk_abs tm =
     let
@@ -941,6 +955,9 @@
 *}
 
 ML {*
+fun matches (ty1, ty2) =
+  Type.raw_instance (ty1, Logic.varifyT ty2);
+
 fun lookup_quot_data lthy qty =
   let
     val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
@@ -986,7 +1003,7 @@
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-  val (alls, exs) = findallex rty qty (prop_of t_a);
+  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
@@ -1000,11 +1017,13 @@
   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+  val t_rv = ObjectLogic.rulify t_r
 in
-  ObjectLogic.rulify t_r
+  Thm.varifyT t_rv
 end
 *}
 
+
 ML {*
   fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
     let