# HG changeset patch
# User wenzelm
# Date 1331719810 -3600
# Node ID 4b2eccaec3f63e099ebee1a95806978c270bc135
# Parent  c2ca2c3d23a689b3d2065068cae9c93dd071b277
more parallel inductive_cases;
more explicit indication of def names;

diff -r c2ca2c3d23a6 -r 4b2eccaec3f6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Mar 14 00:34:56 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Mar 14 11:10:10 2012 +0100
@@ -562,9 +562,12 @@
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val facts = args |> grouped 10 Par_List.map (fn ((a, atts), props) =>
-      ((a, map (prep_att thy) atts),
-        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+    val thmss =
+      map snd args
+      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
+    val facts =
+      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+        args thmss;
   in lthy |> Local_Theory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
@@ -809,7 +812,7 @@
       |> Local_Theory.conceal
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Binding.empty, @{attributes [nitpick_unfold]}),
+         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> Local_Theory.restore_naming lthy;