tuned;
authorwenzelm
Thu Nov 05 23:59:23 2009 +0100 (2009-11-05)
changeset 33459a4a38ed813f7
parent 33458 ae1f5d89b082
child 33466 8f2e102f6628
tuned;
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 22:59:57 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 23:59:23 2009 +0100
     1.3 @@ -338,8 +338,7 @@
     1.4            (DatatypeProp.make_cases new_type_names descr sorts thy2)
     1.5    in
     1.6      thy2
     1.7 -    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
     1.8 -       o Context.Theory
     1.9 +    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
    1.10      |> Sign.parent_path
    1.11      |> store_thmss "cases" new_type_names case_thms
    1.12      |-> (fn thmss => pair (thmss, case_names))
     2.1 --- a/src/HOL/Tools/inductive.ML	Thu Nov 05 22:59:57 2009 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Thu Nov 05 23:59:23 2009 +0100
     2.3 @@ -778,12 +778,14 @@
     2.4  
     2.5      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
     2.6        params intr_ts rec_preds_defs lthy1;
     2.7 -    val elims = if no_elim then [] else
     2.8 -      prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
     2.9 -        unfold rec_preds_defs lthy1;
    2.10 +    val elims =
    2.11 +      if no_elim then []
    2.12 +      else
    2.13 +        prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
    2.14 +          unfold rec_preds_defs lthy1;
    2.15      val raw_induct = zero_var_indexes
    2.16 -      (if no_ind then Drule.asm_rl else
    2.17 -       if coind then
    2.18 +      (if no_ind then Drule.asm_rl
    2.19 +       else if coind then
    2.20           singleton (ProofContext.export
    2.21             (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
    2.22             (rotate_prems ~1 (ObjectLogic.rulify
     3.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 05 22:59:57 2009 +0100
     3.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 05 23:59:23 2009 +0100
     3.3 @@ -520,10 +520,10 @@
     3.4      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     3.5      val (intrs', elims', induct, lthy4) =
     3.6        Inductive.declare_rules kind rec_name coind no_ind cnames
     3.7 -      (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
     3.8 -      (map (fn th => (to_set [] (Context.Proof lthy3) th,
     3.9 -         map fst (fst (Rule_Cases.get th)))) elims)
    3.10 -      raw_induct' lthy3
    3.11 +        (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    3.12 +        (map (fn th => (to_set [] (Context.Proof lthy3) th,
    3.13 +           map fst (fst (Rule_Cases.get th)))) elims)
    3.14 +        raw_induct' lthy3;
    3.15    in
    3.16      ({intrs = intrs', elims = elims', induct = induct,
    3.17        raw_induct = raw_induct', preds = map fst defs},