merged

--- a/src/Doc/Datatypes/Datatypes.thy	Thu Jan 09 21:11:05 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jan 10 12:05:15 2014 +0100
@@ -201,6 +201,7 @@
 
 (*<*)
     hide_const None Some
+    hide_type option
 (*>*)
     datatype_new 'a option = None | Some 'a
 

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 21:11:05 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 12:05:15 2014 +0100
@@ -850,22 +850,22 @@
       let
         val n = 0 upto length ctr_specs
           |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns));
+        val {ctr, disc, ...} = nth ctr_specs n;
         val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
           |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
-        val sel_eqn_opt =
-          find_first (curry (op =) (Binding.name_of fun_binding) o #fun_name) sel_eqns;
+        val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
         val extra_disc_eqn = {
           fun_name = Binding.name_of fun_binding,
           fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
           fun_args = fun_args,
-          ctr = #ctr (nth ctr_specs n),
+          ctr = ctr,
           ctr_no = n,
-          disc = #disc (nth ctr_specs n),
+          disc = disc,
           prems = maps (s_not_conj o #prems) disc_eqns,
           auto_gen = true,
           ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
           code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
-          eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 1000 (*###*),
+          eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (*###*),
           user_eqn = undef_const};
       in
         chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
@@ -1235,7 +1235,8 @@
         val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
         val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
 
-        fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss' disc_thms
+        fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
+            (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
           if null disc_thms orelse null exhaust_thms then
             []
@@ -1250,7 +1251,7 @@
               if prems = [@{term False}] then
                 []
               else
-                mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) fun_args)
+                mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
                   (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
                 |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
@@ -1258,8 +1259,8 @@
                 |> single
             end;
 
-        val disc_iff_thmss = map5 (flat ooo map2 ooo prove_disc_iff) corec_specs exhaust_thmss
-          disc_thmsss' disc_thmsss' disc_eqnss
+        val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
+          disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
           |> map order_list_duplicates;
 
         val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) disc_eqnss

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 21:11:05 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 12:05:15 2014 +0100
@@ -108,10 +108,10 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_disc_iff_tac ctxt frees fun_exhaust fun_disc fun_discss disc_excludes =
+fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_disc fun_discss disc_excludes =
   HEADGOAL (rtac iffI THEN'
     rtac fun_exhaust THEN'
-    K (exhaust_inst_as_projs_tac ctxt frees) THEN'
+    K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
     EVERY' (map (fn [] => etac FalseE
         | [fun_disc'] =>
           if Thm.eq_thm (fun_disc', fun_disc) then