# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265365161 -3600
# Node ID a8518879ee20267abc1615bb0bd6f82879f2257a
# Parent  ffae51f14367919717721ba0bf509b1e0634d4ba
A bit more intelligent and cleaner code.

diff -r ffae51f14367 -r a8518879ee20 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Feb 05 11:09:43 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 11:19:21 2010 +0100
@@ -688,43 +688,61 @@
    those by equality.
    Currently types are not checked so because of the dummyTs it may
    not be complete *)
+fun subst_ty thy ty (rty, qty) r =
+  if r <> NONE then r else
+  case try (Sign.typ_match thy (ty, rty)) Vartab.empty of
+    SOME inst => SOME (Envir.subst_type inst qty)
+  | NONE => NONE
+fun subst_tys thy substs ty =
+  case fold (subst_ty thy ty) substs NONE of
+    SOME ty => ty
+  | NONE =>
+      (case ty of
+        Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
+      | x => x)
+
+fun get_ty_trm_substs ctxt =
+let
+  val thy = ProofContext.theory_of ctxt
+  val quot_infos = Quotient_Info.quotdata_dest ctxt
+  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
+  val const_infos = Quotient_Info.qconsts_dest ctxt
+  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
+  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
+  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
+in
+  (ty_substs, (const_substs @ rel_substs))
+end
+
 fun quotient_lift_all ctxt t =
 let
   val thy = ProofContext.theory_of ctxt
-  val const_infos = Quotient_Info.qconsts_dest ctxt
-  val rel_infos = Quotient_Info.quotdata_dest ctxt
-  fun treat_const_info t qc_info s =
+  val (ty_substs, substs) = get_ty_trm_substs ctxt
+  fun treat_subst t (rt, qt) s =
     if s <> NONE then s else
-      case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of
-        SOME inst => SOME (Envir.subst_term inst (#qconst qc_info))
+      case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
+        SOME inst => SOME (Envir.subst_term inst qt)
       | NONE => NONE;
-  fun treat_const t = fold (treat_const_info t) const_infos NONE
-  fun treat_rel_info t rel_info s =
-    if s <> NONE then s else
-    if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT))
-    else NONE
-  fun treat_rel t = fold (treat_rel_info t) rel_infos NONE
+  fun treat_substs t = fold (treat_subst t) substs NONE
   fun lift_aux t =
-    case treat_const t of
+    case treat_substs t of
       SOME x => x
     | NONE =>
-      (case treat_rel t of
-        SOME x => x
-      | NONE =>
-        (case t of
-          a $ b => lift_aux a $ lift_aux b
-        | Abs(a, T, s) =>
-            let val (y, s') = Term.dest_abs (a, T, s) in
-            Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s')))
-            end
-        | Free(n, _) => Free(n, dummyT)
-        | Var(n, _) => Var(n, dummyT)
-        | Bound i => Bound i
-        | Const(s, _) => Const(s, dummyT)))
+      (case t of
+        a $ b => lift_aux a $ lift_aux b
+      | Abs(a, T, s) =>
+          let val (y, s') = Term.dest_abs (a, T, s) in
+          Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s')))
+          end
+      | Free(n, _) => Free(n, dummyT)
+      | Var(n, _) => Var(n, dummyT)
+      | Bound i => Bound i
+      | Const(s, _) => Const(s, dummyT))
 in
   lift_aux t
 end
 
+
 end; (* structure *)