src/HOL/SPARK/Tools/spark_vcs.ML

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Jul 18 20:54:56 2015 +0200
@@ -206,22 +206,22 @@
     val UNIV_eq = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
-      (fn _ =>
-         rtac @{thm subset_antisym} 1 THEN
-         rtac @{thm subsetI} 1 THEN
-         Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info
-           (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
-         ALLGOALS (asm_full_simp_tac lthy));
+      (fn {context = ctxt, ...} =>
+         resolve_tac ctxt @{thms subset_antisym} 1 THEN
+         resolve_tac ctxt @{thms subsetI} 1 THEN
+         Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info
+           (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
+         ALLGOALS (asm_full_simp_tac ctxt));
 
     val finite_UNIV = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (Const (@{const_name finite},
          HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
-      (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1);
+      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
 
     val card_UNIV = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (card, HOLogic.mk_number HOLogic.natT k)))
-      (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1);
+      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
 
     val range_pos = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -232,20 +232,20 @@
             HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
               HOLogic.mk_number HOLogic.intT 0 $
               (@{term int} $ card))))
-      (fn _ =>
-         simp_tac (lthy addsimps [card_UNIV]) 1 THEN
-         simp_tac (lthy addsimps [UNIV_eq, def1]) 1 THEN
-         rtac @{thm subset_antisym} 1 THEN
-         simp_tac lthy 1 THEN
-         rtac @{thm subsetI} 1 THEN
-         asm_full_simp_tac (lthy addsimps @{thms interval_expand}
+      (fn {context = ctxt, ...} =>
+         simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
+         simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
+         resolve_tac ctxt @{thms subset_antisym} 1 THEN
+         simp_tac ctxt 1 THEN
+         resolve_tac ctxt @{thms subsetI} 1 THEN
+         asm_full_simp_tac (ctxt addsimps @{thms interval_expand}
            delsimps @{thms atLeastLessThan_iff}) 1);
 
     val lthy' =
       Class.prove_instantiation_instance (fn ctxt =>
         Class.intro_classes_tac ctxt [] THEN
-        rtac finite_UNIV 1 THEN
-        rtac range_pos 1 THEN
+        resolve_tac ctxt [finite_UNIV] 1 THEN
+        resolve_tac ctxt [range_pos] 1 THEN
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;
 
@@ -254,23 +254,24 @@
         val n = HOLogic.mk_number HOLogic.intT i;
         val th = Goal.prove lthy' [] []
           (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
-          (fn _ => simp_tac (lthy' addsimps [def1]) 1);
+          (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);
         val th' = Goal.prove lthy' [] []
           (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
-          (fn _ =>
-             rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN
-             simp_tac (lthy' addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
+          (fn {context = ctxt, ...} =>
+             resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN
+             simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
       in (th, th') end) cs);
 
     val first_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (Const (@{const_name first_el}, T), hd cs)))
-      (fn _ => simp_tac (lthy' addsimps [@{thm first_el_def}, hd val_eqs]) 1);
+      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
 
     val last_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (Const (@{const_name last_el}, T), List.last cs)))
-      (fn _ => simp_tac (lthy' addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
+      (fn {context = ctxt, ...} =>
+        simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   in
     lthy' |>
     Local_Theory.note