# HG changeset patch
# User traytel
# Date 1389352151 -3600
# Node ID d72279b9bc4467edf47905e772b800c886ab916f
# Parent  30ded82ff8067a78f0e1bebed59d1ced5390a409
use the right context in tactic

diff -r 30ded82ff806 -r d72279b9bc44 src/HOL/BNF/Tools/bnf_decl.ML
--- a/src/HOL/BNF/Tools/bnf_decl.ML	Fri Jan 10 09:48:11 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_decl.ML	Fri Jan 10 12:09:11 2014 +0100
@@ -64,18 +64,19 @@
 
     fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
-    fun mk_wit_thms set_maps =
-      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
-        |> Conjunction.elim_balanced (length wit_goals)
-        |> map2 (Conjunction.elim_balanced o length) wit_goalss
-        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
 
     val ((_, [thms]), (lthy_old, lthy)) = Local_Theory.background_theory_result
       (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), goals)]) lthy
       ||> `Local_Theory.restore;
+
+    fun mk_wit_thms set_maps =
+      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+      |> Conjunction.elim_balanced (length wit_goals)
+      |> map2 (Conjunction.elim_balanced o length) wit_goalss
+      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
-    BNF_Def.register_bnf key (after_qed mk_wit_thms (map single  (Morphism.fact phi thms)) lthy)
+    BNF_Def.register_bnf key (after_qed mk_wit_thms (map single (Morphism.fact phi thms)) lthy)
   end;
 
 val bnf_decl = prepare_decl (K I) (K I);