# HG changeset patch
# User blanchet
# Date 1382333058 -7200
# Node ID 8039bd7e98b1e9316403135c797d752a8ade6d9d
# Parent  83145b857bb97749f1bc64c15bd884364abd4f41
systematically close derivations in BNF package

diff -r 83145b857bb9 -r 8039bd7e98b1 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 23:36:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 07:24:18 2013 +0200
@@ -362,7 +362,8 @@
             (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map (fn (user_eqn, num_extra_args, rec_thm) =>
             mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
-            |> K |> Goal.prove lthy [] [] user_eqn);
+            |> K |> Goal.prove lthy [] [] user_eqn
+            |> Thm.close_derivation);
         val poss = find_indices (fn (x, y) => #ctr x = #ctr y) fun_data eqns_data;
       in
         (poss, simp_thmss)
@@ -896,7 +897,7 @@
 *)
 
     val exclss'' = exclss' |> map (map (fn (idx, t) =>
-      (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
+      (idx, (Option.map (Goal.prove lthy [] [] t |> Thm.close_derivation) (excl_tac idx), t))));
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     val (obligation_idxss, obligationss) = exclss''
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
@@ -930,6 +931,7 @@
               if prems = [@{term False}] then [] else
               mk_primcorec_disc_tac lthy def_thms disc_corec k m exclsss
               |> K |> Goal.prove lthy [] [] t
+              |> Thm.close_derivation
               |> pair (#disc (nth ctr_specs ctr_no))
               |> single
             end;
@@ -958,6 +960,7 @@
             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
               nested_map_idents nested_map_comps sel_corec k m exclsss
             |> K |> Goal.prove lthy [] [] t
+            |> Thm.close_derivation
             |> pair sel
           end;
 
@@ -995,6 +998,7 @@
               if prems = [@{term False}] then [] else
                 mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
                 |> K |> Goal.prove lthy [] [] t
+                |> Thm.close_derivation
                 |> pair ctr
                 |> single
             end;
@@ -1065,10 +1069,12 @@
 
                 val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms
-                  |> K |> Goal.prove lthy [] [] raw_t;
+                  |> K |> Goal.prove lthy [] [] raw_t
+                  |> Thm.close_derivation;
               in
                 mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
                 |> K |> Goal.prove lthy [] [] t
+                |> Thm.close_derivation
                 |> single
               end)
           end;