src/Tools/atomize_elim.ML

--- a/src/Tools/atomize_elim.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/atomize_elim.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -120,7 +120,7 @@
               val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
                          @{thm meta_spec}
             in
-              compose_tac (false, rule, 1) i
+              compose_tac ctxt (false, rule, 1) i
             end
     in
       quantify_thesis