tuned
authorhaftmann
Mon Sep 28 14:54:15 2009 +0200 (2009-09-28)
changeset 327303958b45b29e4
parent 32729 1441cf4ddc1a
child 32731 f7ed14d60818
tuned
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 14:48:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 14:54:15 2009 +0200
     1.3 @@ -320,15 +320,14 @@
     1.4      split = split,
     1.5      split_asm = split_asm});
     1.6  
     1.7 -fun add_rules simps case_rewrites rec_rewrites inject distinct
     1.8 -                  weak_case_congs cong_att =
     1.9 +fun add_rules inject distinct rec_rewrites case_rewrites  weak_case_congs simps =
    1.10    PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.11      ((Binding.empty, flat case_rewrites @
    1.12            flat distinct @ rec_rewrites), [Simplifier.simp_add]),
    1.13      ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
    1.14      ((Binding.empty, flat inject), [iff_add]),
    1.15      ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.16 -    ((Binding.empty, weak_case_congs), [cong_att])]
    1.17 +    ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
    1.18    #> snd;
    1.19  
    1.20  fun add_cases_induct infos inducts thy =
    1.21 @@ -370,22 +369,22 @@
    1.22      val (split_thms, thy9) = DatatypeAbsProofs.prove_split_thms
    1.23        config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
    1.24  
    1.25 -    val simps = flat (distinct_rules @ inject @ case_rewrites) @ rec_rewrites;
    1.26 +    val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
    1.27      val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.28        (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
    1.29          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ split_thms);
    1.30      val dt_names = map fst dt_infos;
    1.31    in
    1.32      thy9
    1.33 -    |> add_case_tr' case_names
    1.34      |> Sign.add_path (space_implode "_" new_type_names)
    1.35 -    |> add_rules simps case_rewrites rec_rewrites inject distinct_rules
    1.36 -         weak_case_congs (Simplifier.attrib (op addcongs))
    1.37 -    |> register dt_infos
    1.38 +    |> add_rules inject distinct_rules rec_rewrites case_rewrites
    1.39 +         weak_case_congs simps
    1.40      |> add_cases_induct dt_infos inducts
    1.41 -    |> Sign.parent_path
    1.42      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.43      |> snd
    1.44 +    |> Sign.parent_path
    1.45 +    |> add_case_tr' case_names
    1.46 +    |> register dt_infos
    1.47      |> DatatypeInterpretation.data (config, dt_names)
    1.48      |> pair dt_names
    1.49    end;