diff -r dde8ad700c5b -r 6deecec6795f Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Feb 05 11:28:49 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 11:37:18 2010 +0100
@@ -683,11 +683,14 @@
   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
@@ -721,7 +724,6 @@
   (ty_substs, (const_substs @ rel_substs))
 end
 
-
 fun quotient_lift_all ctxt t =
 let
   val thy = ProofContext.theory_of ctxt
@@ -732,19 +734,23 @@
     | 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')))
+      | 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, _) => Free(n, dummyT)
-      | Var(n, _) => Var(n, dummyT)
+      | 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, _) => Const(s, dummyT))
+      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
 in
   lift_aux t
 end
 
 
+
 end; (* structure *)