src/HOL/Tools/Quotient/quotient_type.ML

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -51,7 +51,7 @@
 
 
 (* 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
@@ -62,7 +62,7 @@
       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
 
@@ -74,7 +74,7 @@
     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