diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -530,17 +530,19 @@
 
 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
 
-fun copy_prems_tac [] ns i =
-    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
-  | copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
-  | copy_prems_tac (m :: ms) ns i =
-    eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
+fun copy_prems_tac ctxt [] ns i =
+    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i
+  | copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i
+  | copy_prems_tac ctxt (m :: ms) ns i =
+    eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i
 
 (* Metis generates variables of the form _nnn. *)
 val is_metis_fresh_variable = String.isPrefix "_"
 
-fun instantiate_forall_tac thy t i st =
+fun instantiate_forall_tac ctxt t i st =
   let
+    val thy = Proof_Context.theory_of ctxt
+
     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
 
     fun repair (t as (Var ((s, _), _))) =
@@ -581,16 +583,16 @@
         end
       | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   in
-    (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
+    (DETERM (eresolve_tac ctxt @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   end
 
-fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
+fun fix_exists_tac ctxt t = eresolve_tac ctxt [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
 
-fun release_quantifier_tac thy (skolem, t) =
-  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
+fun release_quantifier_tac ctxt (skolem, t) =
+  (if skolem then fix_exists_tac ctxt else instantiate_forall_tac ctxt) t
 
 fun release_clusters_tac _ _ _ [] = K all_tac
-  | release_clusters_tac thy ax_counts substs ((ax_no, cluster_no) :: clusters) =
+  | release_clusters_tac ctxt ax_counts substs ((ax_no, cluster_no) :: clusters) =
     let
       val cluster_of_var = Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
       fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
@@ -605,13 +607,13 @@
                           else
                             NONE)
       fun do_cluster_subst cluster_subst =
-        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
+        map (release_quantifier_tac ctxt) cluster_subst @ [rotate_tac 1]
       val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
     in
       rotate_tac first_prem
       THEN' (EVERY' (maps do_cluster_subst cluster_substs))
       THEN' rotate_tac (~ first_prem - length cluster_substs)
-      THEN' release_clusters_tac thy ax_counts substs clusters
+      THEN' release_clusters_tac ctxt ax_counts substs clusters
     end
 
 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
@@ -731,21 +733,20 @@
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_of_subst_info substs))
 *)
+      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
 
       fun cut_and_ex_tac axiom =
-        cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
+        cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1)
       fun rotation_of_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
-
-      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
     in
       Goal.prove ctxt' [] [] @{prop False}
         (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts)
               THEN rename_tac outer_param_names 1
-              THEN copy_prems_tac (map snd ax_counts) [] 1)
-            THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
+              THEN copy_prems_tac ctxt' (map snd ax_counts) [] 1)
+            THEN release_clusters_tac ctxt' ax_counts substs ordered_clusters 1
             THEN match_tac ctxt' [prems_imp_false] 1
-            THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
+            THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i
               THEN rotate_tac (rotation_of_subgoal i) i
               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
               THEN assume_tac ctxt' i