merged

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 17:01:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 17:08:57 2013 +0200
@@ -8,8 +8,15 @@
 signature BNF_CTR_SUGAR =
 sig
   type ctr_wrap_result =
-    term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
-    thm list list
+    {discs: term list,
+     selss: term list list,
+     exhaust: thm,
+     injects: thm list,
+     distincts: thm list,
+     case_thms: thm list,
+     disc_thmss: thm list list,
+     discIs: thm list,
+     sel_thmss: thm list list};
 
   val rep_compat_prefix: string
 
@@ -37,8 +44,15 @@
 open BNF_Ctr_Sugar_Tactics
 
 type ctr_wrap_result =
-  term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
-  thm list list;
+  {discs: term list,
+   selss: term list list,
+   exhaust: thm,
+   injects: thm list,
+   distincts: thm list,
+   case_thms: thm list,
+   disc_thmss: thm list list,
+   discIs: thm list,
+   sel_thmss: thm list list};
 
 val rep_compat_prefix = "new";
 
@@ -671,14 +685,15 @@
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
       in
-        ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
-          sel_thmss),
-          lthy
-          |> not rep_compat ?
-             (Local_Theory.declaration {syntax = false, pervasive = true}
+        ({discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms,
+          distincts = distinct_thms, case_thms = case_thms, disc_thmss = disc_thmss,
+          discIs = discI_thms, sel_thmss = sel_thmss},
+         lthy
+         |> not rep_compat ?
+            (Local_Theory.declaration {syntax = false, pervasive = true}
                (fn phi => Case_Translation.register
-                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
-          |> Local_Theory.notes (notes' @ notes) |> snd)
+                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
+         |> Local_Theory.notes (notes' @ notes) |> snd)
       end;
   in
     (goalss, after_qed, lthy')

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 17:01:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 17:08:57 2013 +0200
@@ -8,21 +8,21 @@
 signature BNF_FP =
 sig
   type fp_result =
-    {bnfs : BNF_Def.BNF list,
-     dtors : term list,
-     ctors : term list,
-     folds : term list,
-     recs : term list,
-     induct : thm,
-     strong_induct : thm,
-     dtor_ctors : thm list,
-     ctor_dtors : thm list,
-     ctor_injects : thm list,
-     map_thms : thm list,
-     set_thmss : thm list list,
-     rel_thms : thm list,
-     fold_thms : thm list,
-     rec_thms : thm list}
+    {bnfs: BNF_Def.BNF list,
+     dtors: term list,
+     ctors: term list,
+     folds: term list,
+     recs: term list,
+     induct: thm,
+     strong_induct: thm,
+     dtor_ctors: thm list,
+     ctor_dtors: thm list,
+     ctor_injects: thm list,
+     map_thms: thm list,
+     set_thmss: thm list list,
+     rel_thms: thm list,
+     fold_thms: thm list,
+     rec_thms: thm list}
 
   val time: Timer.real_timer -> string -> Timer.real_timer
 
@@ -168,21 +168,21 @@
 open BNF_Util
 
 type fp_result =
-  {bnfs : BNF_Def.BNF list,
-   dtors : term list,
-   ctors : term list,
-   folds : term list,
-   recs : term list,
-   induct : thm,
-   strong_induct : thm,
-   dtor_ctors : thm list,
-   ctor_dtors : thm list,
-   ctor_injects : thm list,
-   map_thms : thm list,
-   set_thmss : thm list list,
-   rel_thms : thm list,
-   fold_thms : thm list,
-   rec_thms : thm list};
+  {bnfs: BNF_Def.BNF list,
+   dtors: term list,
+   ctors: term list,
+   folds: term list,
+   recs: term list,
+   induct: thm,
+   strong_induct: thm,
+   dtor_ctors: thm list,
+   ctor_dtors: thm list,
+   ctor_injects: thm list,
+   map_thms: thm list,
+   set_thmss: thm list list,
+   rel_thms: thm list,
+   fold_thms: thm list,
+   rec_thms: thm list};
 
 val timing = true;
 fun time timer msg = (if timing

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:01:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:08:57 2013 +0200
@@ -369,12 +369,12 @@
 
     val fp_b_names = map base_name_of_typ fpTs;
 
-    val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
-    val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
-    val exhaust_thms = map #3 ctr_wrap_ress;
-    val disc_thmsss = map #7 ctr_wrap_ress;
-    val discIss = map #8 ctr_wrap_ress;
-    val sel_thmsss = map #9 ctr_wrap_ress;
+    val discss = map (map (mk_disc_or_sel As) o #discs) ctr_wrap_ress;
+    val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_wrap_ress;
+    val exhausts = map #exhaust ctr_wrap_ress;
+    val disc_thmsss = map #disc_thmss ctr_wrap_ress;
+    val discIss = map #discIs ctr_wrap_ress;
+    val sel_thmsss = map #sel_thmss ctr_wrap_ress;
 
     val (((rs, us'), vs'), names_lthy) =
       lthy
@@ -440,7 +440,7 @@
         fun prove dtor_coinduct' goal =
           Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
             mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
-              exhaust_thms ctr_defss disc_thmsss sel_thmsss)
+              exhausts ctr_defss disc_thmsss sel_thmsss)
           |> singleton (Proof_Context.export names_lthy lthy)
           |> Thm.close_derivation;
 
@@ -1202,8 +1202,8 @@
 
     (* TODO: Add map, sets, rel simps *)
     val mk_simp_thmss =
-      map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
-        injects @ distincts @ cases @ rec_likes @ fold_likes);
+      map3 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes =>
+        injects @ distincts @ case_thms @ rec_likes @ fold_likes);
 
     fun derive_and_note_induct_fold_rec_thms_for_types
         (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =