src/HOL/Tools/Quotient/quotient_type.ML

       (typedef_term rel rty lthy) NONE typedef_tac lthy
   end
 
 
 (* tactic to prove the quot_type theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
+fun typedef_quot_type_tac ctxt equiv_thm ((_, typedef_info): Typedef.info) =
   let
     val rep_thm = #Rep typedef_info RS mem_def1
     val rep_inv = #Rep_inverse typedef_info
     val abs_inv = #Abs_inverse typedef_info
     val rep_inj = #Rep_inject typedef_info
   in
     (rtac @{thm quot_type.intro} THEN' RANGE [
       rtac equiv_thm,
       rtac rep_thm,
       rtac rep_inv,
-      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
+      rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt,
       rtac rep_inj]) 1
   end
 
 (* proves the quot_type theorem for the new type *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =

     val quot_type_const = Const (@{const_name "quot_type"},
       fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
     val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   in
     Goal.prove lthy [] [] goal
-      (K (typedef_quot_type_tac equiv_thm typedef_info))
+      (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
   end
    
 open Lifting_Util
 
 infix 0 MRSL