# HG changeset patch
# User blanchet
# Date 1380196567 -7200
# Node ID 6f9dbc063ae6cdd5205d120bdb999595042ca68a
# Parent  0fc622be018571a1859437396d10d66ad839a671
tuning

diff -r 0fc622be0185 -r 6f9dbc063ae6 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 13:56:07 2013 +0200
@@ -811,7 +811,7 @@
                   |> Thm.close_derivation
                 end;
 
-              val expand_thms =
+              val expand_thm =
                 let
                   fun mk_prems k udisc usels vdisc vsels =
                     (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
@@ -829,12 +829,12 @@
                   val uncollapse_thms =
                     map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
                 in
-                  [Goal.prove_sorry lthy [] [] goal (fn _ =>
-                     mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
-                       (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
-                       disc_exclude_thmsss')]
-                  |> map Thm.close_derivation
-                  |> Proof_Context.export names_lthy lthy
+                  Goal.prove_sorry lthy [] [] goal (fn _ =>
+                    mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
+                      (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
+                      disc_exclude_thmsss')
+                  |> Thm.close_derivation
+                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
 
               val (sel_split_thm, sel_split_asm_thm) =
@@ -849,20 +849,20 @@
                   (thm, asm_thm)
                 end;
 
-              val case_conv_if_thms =
+              val case_conv_if_thm =
                 let
                   val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
                 in
-                  [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
-                     mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
-                  |> map Thm.close_derivation
-                  |> Proof_Context.export names_lthy lthy
+                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+                    mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+                  |> Thm.close_derivation
+                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
             in
               (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
                nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
-               all_collapse_thms, safe_collapse_thms, expand_thms, [sel_split_thm],
-               [sel_split_asm_thm], case_conv_if_thms)
+               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
+               [sel_split_asm_thm], [case_conv_if_thm])
             end;
 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));