--- a/Quot/quotient_term.ML	Thu Feb 04 17:58:23 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Feb 04 18:09:20 2010 +0100
@@ -25,6 +25,8 @@
 
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
+
+  val quotient_lift_all: Proof.context -> term -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -681,6 +683,48 @@
   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 *)
+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
+  fun lift_aux t =
+    case treat_const 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)))
+in
+  lift_aux t
+end
+
 end; (* structure *)