--- a/Quot/quotient_term.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -689,48 +689,74 @@
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
-(* Finds subterms of a term that are lifted to constants and replaces
-   those as well as occurrences of the equivalence relation and replaces
-   those by equality.
-   Currently types are not checked so because of the dummyTs it may
-   not be complete *)
+(*** Translating the goal automatically
+
+Finds subterms of a term that can be lifted and:
+* replaces subterms matching lifted constants by the lifted constants
+* replaces equivalence relations by equalities
+* In constants, frees and schematic variables replaces
+  subtypes matching lifted types by those types *)
+
+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 subst_trm thy t (rt, qt) s =
+  if s <> NONE then s else
+    case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
+      SOME inst => SOME (Envir.subst_term inst qt)
+    | NONE => NONE;
+fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
+
+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 =
-    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))
-      | 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
+  val (ty_substs, substs) = get_ty_trm_substs ctxt
   fun lift_aux t =
-    case treat_const t of
+    case subst_trms thy 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, ty, s) =>
+          let
+            val (y, s') = Term.dest_abs (a, ty, s)
+            val nty = subst_tys thy ty_substs ty
+          in
+          Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s')))
+          end
+      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
+      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
+      | Bound i => Bound i
+      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
 in
   lift_aux t
 end
 
+
+
 end; (* structure *)