src/HOL/Tools/datatype_package.ML
changeset 19599 a5c7eb37d14f
parent 19539 5b37bb0ad964
child 19716 52c22fccdaaf
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 09 10:09:17 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 09 10:09:37 2006 +0200
     1.3 @@ -139,14 +139,6 @@
     1.4          in SOME (map mk_co cos) end
     1.5      | NONE => NONE;
     1.6  
     1.7 -fun get_case_const_data thy c =
     1.8 -  case find_first (fn (_, {index, descr, case_name, ...}) =>
     1.9 -      case_name = c
    1.10 -    ) ((Symtab.dest o get_datatypes) thy)
    1.11 -   of NONE => NONE
    1.12 -    | SOME (_, {index, descr, ...}) =>
    1.13 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    1.14 -
    1.15  fun find_tname var Bi =
    1.16    let val frees = map dest_Free (term_frees Bi)
    1.17        val params = rename_wrt_term Bi (Logic.strip_params Bi);
    1.18 @@ -717,9 +709,10 @@
    1.19        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.20        |> add_cases_induct dt_infos induct
    1.21        |> Theory.parent_path
    1.22 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.23 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.24 +      |> snd
    1.25        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.26 -      |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names';
    1.27 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    1.28    in
    1.29      ({distinct = distinct,
    1.30        inject = inject,
    1.31 @@ -778,7 +771,7 @@
    1.32        |> Theory.parent_path
    1.33        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.34        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.35 -      |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names;
    1.36 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    1.37    in
    1.38      ({distinct = distinct,
    1.39        inject = inject,
    1.40 @@ -876,15 +869,18 @@
    1.41  
    1.42      val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.43  
    1.44 -    val thy11 = thy10 |>
    1.45 -      Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.46 -      add_rules simps case_thms size_thms rec_thms inject distinct
    1.47 -        weak_case_congs (Simplifier.attrib (op addcongs)) |> 
    1.48 -      put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.49 -      add_cases_induct dt_infos induction' |>
    1.50 -      Theory.parent_path |>
    1.51 -      (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.52 -      DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.53 +    val thy11 =
    1.54 +      thy10
    1.55 +      |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, [])
    1.56 +      |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.57 +           weak_case_congs (Simplifier.attrib (op addcongs))
    1.58 +      |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.59 +      |> add_cases_induct dt_infos induction'
    1.60 +      |> Theory.parent_path
    1.61 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.62 +      |> snd
    1.63 +      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.64 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    1.65    in
    1.66      ({distinct = distinct,
    1.67        inject = inject,