--- a/Quot/quotient_term.ML	Fri Feb 05 11:19:21 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 11:28:49 2010 +0100
@@ -701,6 +701,13 @@
         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
@@ -714,18 +721,13 @@
   (ty_substs, (const_substs @ rel_substs))
 end
 
+
 fun quotient_lift_all ctxt t =
 let
   val thy = ProofContext.theory_of ctxt
   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, rt)) (Vartab.empty, Vartab.empty) of
-        SOME inst => SOME (Envir.subst_term inst qt)
-      | NONE => NONE;
-  fun treat_substs t = fold (treat_subst t) substs NONE
   fun lift_aux t =
-    case treat_substs t of
+    case subst_trms thy substs t of
       SOME x => x
     | NONE =>
       (case t of