src/HOL/Tools/inductive.ML
changeset 46915 4b2eccaec3f6
parent 46893 d5bb4c212df1
child 46947 b8c7eb0c2f89
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Mar 14 00:34:56 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Mar 14 11:10:10 2012 +0100
     1.3 @@ -562,9 +562,12 @@
     1.4  fun gen_inductive_cases prep_att prep_prop args lthy =
     1.5    let
     1.6      val thy = Proof_Context.theory_of lthy;
     1.7 -    val facts = args |> grouped 10 Par_List.map (fn ((a, atts), props) =>
     1.8 -      ((a, map (prep_att thy) atts),
     1.9 -        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
    1.10 +    val thmss =
    1.11 +      map snd args
    1.12 +      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
    1.13 +    val facts =
    1.14 +      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    1.15 +        args thmss;
    1.16    in lthy |> Local_Theory.notes facts |>> map snd end;
    1.17  
    1.18  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    1.19 @@ -809,7 +812,7 @@
    1.20        |> Local_Theory.conceal
    1.21        |> Local_Theory.define
    1.22          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    1.23 -         ((Binding.empty, @{attributes [nitpick_unfold]}),
    1.24 +         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
    1.25             fold_rev lambda params
    1.26               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
    1.27        ||> Local_Theory.restore_naming lthy;