# HG changeset patch
# User traytel
# Date 1348999696 -7200
# Node ID 44d85dc8ca08b35b18b77b4c889ae7c81080b5fc
# Parent  5eb0b0d389eac1a621f8967ce03708e755245902
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;

diff -r 5eb0b0d389ea -r 44d85dc8ca08 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 12:04:47 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 12:08:16 2012 +0200
@@ -389,6 +389,7 @@
                 Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
           in
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
+            |> Thm.close_derivation
           end;
 
         val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
@@ -475,7 +476,9 @@
                       [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
                          HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
 
-                  fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
+                  fun prove tac goal =
+                    Skip_Proof.prove lthy [] [] goal (K tac)
+                    |> Thm.close_derivation;
 
                   val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
 
@@ -501,6 +504,7 @@
                 in
                   Skip_Proof.prove lthy [] [] goal (fn _ =>
                     mk_disc_exhaust_tac n exhaust_thm discI_thms)
+                  |> Thm.close_derivation
                 end;
 
               val (collapse_thms, collapse_thm_opts) =
@@ -519,6 +523,7 @@
                   map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
                     Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
                       mk_collapse_tac ctxt m discD sel_thms)
+                    |> Thm.close_derivation
                     |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
                   |> `(map_filter I)
                 end;
@@ -542,11 +547,12 @@
                   val uncollapse_thms =
                     map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
                 in
-                  [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                     mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm)
+                  [Skip_Proof.prove lthy [] [] goal (fn _ =>
+                     mk_expand_tac n ms (inst_thm u disc_exhaust_thm)
                        (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
                        disc_exclude_thmsss')]
                   |> Proof_Context.export names_lthy lthy
+                  |> map Thm.close_derivation
                 end;
 
               val case_conv_thms =
@@ -557,6 +563,7 @@
                   [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
                      mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
                   |> Proof_Context.export names_lthy lthy
+                  |> map Thm.close_derivation
                 end;
             in
               (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
@@ -576,7 +583,7 @@
           in
             (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
              Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1)))
-            |> pairself (singleton (Proof_Context.export names_lthy lthy))
+            |> pairself (singleton (Proof_Context.export names_lthy lthy) #> Thm.close_derivation)
           end;
 
         val (split_thm, split_asm_thm) =
@@ -599,10 +606,12 @@
               Skip_Proof.prove lthy [] [] goal
                 (fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss)
               |> singleton (Proof_Context.export names_lthy lthy)
+              |> Thm.close_derivation;
             val split_asm_thm =
               Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} =>
                 mk_split_asm_tac ctxt split_thm)
               |> singleton (Proof_Context.export names_lthy lthy)
+              |> Thm.close_derivation;
           in
             (split_thm, split_asm_thm)
           end;
@@ -644,7 +653,7 @@
   end;
 
 fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
-  map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
+  map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss
   |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
 
 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
diff -r 5eb0b0d389ea -r 44d85dc8ca08 src/HOL/BNF/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Sun Sep 30 12:04:47 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Sun Sep 30 12:08:16 2012 +0200
@@ -13,8 +13,8 @@
     tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
-  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
-    thm list list list -> thm list list list -> tactic
+  val mk_expand_tac: int -> int list -> thm -> thm -> thm list -> thm list list list ->
+    thm list list list -> tactic
   val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_disc_exclude_tac: thm -> tactic
@@ -66,8 +66,7 @@
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
 
-fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
-    disc_excludesss' =
+fun mk_expand_tac n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss disc_excludesss' =
   if ms = [0] then
     rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1
   else