src/HOL/Tools/Lifting/lifting_term.ML

     val abs_type = fastype_of abs  
   in
     (domain_type abs_type, range_type abs_type)
   end
 
-fun prove_quot_theorem ctxt (rty, qty) =
+fun prove_quot_theorem' ctxt (rty, qty) =
   case (rty, qty) of
     (Type (s, tys), Type (s', tys')) =>
       if s = s'
       then
         let
-          val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+          val args = map (prove_quot_theorem' ctxt) (tys ~~ tys')
         in
           if forall is_id_quot args
           then
             @{thm identity_quotient}
           else

         let
           val quot_thm = get_quot_thm ctxt s'
           val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
           val qtyenv = match ctxt equiv_match_err qty_pat qty
           val rtys' = map (Envir.subst_type qtyenv) rtys
-          val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+          val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
         in
           if forall is_id_quot args
           then
             quot_thm
           else

     val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
   in
     Thm.instantiate (ty_inst, []) quot_thm
   end
 
-fun absrep_fun ctxt (rty, qty) = 
+fun prove_quot_theorem ctxt (rty, qty) =
   let
     val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
+    val quot_thm = prove_quot_theorem' ctxt (rty, qty)
   in
-    quot_thm_abs forced_quot_thm
+    force_qty_type thy qty quot_thm
   end
 
+fun absrep_fun ctxt (rty, qty) =
+  quot_thm_abs (prove_quot_theorem ctxt (rty, qty))
+
 fun equiv_relation ctxt (rty, qty) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
-  in
-    quot_thm_rel forced_quot_thm
-  end
+  quot_thm_rel (prove_quot_theorem ctxt (rty, qty))
 
 end;