src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 25 23:01:31 2015 +0200
@@ -1148,7 +1148,7 @@
 
     fun exclude_tac tac_opt sequential (c, c', a) =
       if a orelse c = c' orelse sequential then
-        SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
+        SOME (fn {context = ctxt, prems = _} => HEADGOAL (mk_primcorec_assumption_tac ctxt []))
       else
         tac_opt;
 
@@ -1233,9 +1233,11 @@
           |> list_all_fun_args ps
           |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
               | [nchotomy_thm] => fn [goal] =>
-                [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
-                   (length disc_eqns) nchotomy_thm
-                 |> K |> Goal.prove_sorry lthy [] [] goal
+                [Goal.prove_sorry lthy [] [] goal
+                  (fn {context = ctxt, prems = _} =>
+                    mk_primcorec_exhaust_tac ctxt
+                      ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
+                      (length disc_eqns) nchotomy_thm)
                  |> Thm.close_derivation])
             disc_eqnss nchotomy_thmss;
         val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
@@ -1267,8 +1269,9 @@
               if prems = [@{term False}] then
                 []
               else
-                mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
-                |> K |> Goal.prove_sorry lthy [] [] goal
+                Goal.prove_sorry lthy [] [] goal
+                  (fn {context = ctxt, prems = _} =>
+                    mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss)
                 |> Thm.close_derivation
                 |> pair (#disc (nth ctr_specs ctr_no))
                 |> pair eqn_pos
@@ -1297,9 +1300,10 @@
               |> curry Logic.list_all (map dest_Free fun_args);
             val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term;
           in
-            mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps
-              fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss
-            |> K |> Goal.prove_sorry lthy [] [] goal
+            Goal.prove_sorry lthy [] [] goal
+              (fn {context = ctxt, prems = _} =>
+                mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms
+                fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss)
             |> Thm.close_derivation
             |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
             |> pair sel
@@ -1346,8 +1350,9 @@
               if prems = [@{term False}] then
                 []
               else
-                mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
-                |> K |> Goal.prove_sorry lthy [] [] goal
+                Goal.prove_sorry lthy [] [] goal
+                  (fn {context = ctxt, prems = _} =>
+                    mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)
                 |> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*)
                 |> Thm.close_derivation
                 |> pair ctr
@@ -1431,14 +1436,16 @@
                     val (distincts, discIs, _, split_sels, split_sel_asms) =
                       case_thms_of_term lthy raw_rhs;
 
-                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels
-                        split_sel_asms ms ctr_thms
-                        (if exhaustive_code then try the_single nchotomys else NONE)
-                      |> K |> Goal.prove_sorry lthy [] [] raw_goal
+                    val raw_code_thm = 
+                      Goal.prove_sorry lthy [] [] raw_goal
+                        (fn {context = ctxt, prems = _} =>
+                          mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
+                            ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE))
                       |> Thm.close_derivation;
                   in
-                    mk_primcorec_code_tac lthy distincts split_sels raw_code_thm
-                    |> K |> Goal.prove_sorry lthy [] [] goal
+                    Goal.prove_sorry lthy [] [] goal
+                      (fn {context = ctxt, prems = _} =>
+                        mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm)
                     |> Thm.close_derivation
                     |> single
                   end)
@@ -1465,9 +1472,10 @@
                   mk_conjs prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
             in
-              mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
-                (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
-              |> K |> Goal.prove_sorry lthy [] [] goal
+              Goal.prove_sorry lthy [] [] goal
+                (fn {context = ctxt, prems = _} =>
+                  mk_primcorec_disc_iff_tac ctxt (map (fst o dest_Free) exhaust_fun_args)
+                    (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss))
               |> Thm.close_derivation
               |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}