src/HOL/Tools/datatype_package.ML
changeset 19716 52c22fccdaaf
parent 19599 a5c7eb37d14f
child 19841 f2fa72c13186
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed May 24 22:15:07 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed May 24 22:44:56 2006 +0200
     1.3 @@ -573,6 +573,11 @@
     1.4      in (Theory.parent_path thy'', axs::axss)
     1.5      end) (thy, []) (tnames ~~ tss) |> swap;
     1.6  
     1.7 +fun specify_consts args thy =
     1.8 +  let val specs =
     1.9 +    args |> map (fn (c, T, mx) => Const (Sign.full_name thy (Syntax.const_name c mx), T));
    1.10 +  in thy |> Theory.add_consts_i args |> Theory.add_finals_i false specs end;
    1.11 +
    1.12  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.13      case_names_induct case_names_exhausts thy =
    1.14    let
    1.15 @@ -623,24 +628,22 @@
    1.16  
    1.17        (** primrec combinators **)
    1.18  
    1.19 -      Theory.add_consts_i (map (fn ((name, T), T') =>
    1.20 -        (name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
    1.21 -          (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
    1.22 +      specify_consts (map (fn ((name, T), T') =>
    1.23 +        (name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
    1.24  
    1.25        (** case combinators **)
    1.26  
    1.27 -      Theory.add_consts_i (map (fn ((name, T), Ts) =>
    1.28 -        (name, Ts @ [T] ---> freeT, NoSyn))
    1.29 -          (case_names ~~ newTs ~~ case_fn_Ts));
    1.30 +      specify_consts (map (fn ((name, T), Ts) =>
    1.31 +        (name, Ts @ [T] ---> freeT, NoSyn)) (case_names ~~ newTs ~~ case_fn_Ts));
    1.32  
    1.33 -    val reccomb_names' = map (Sign.intern_const thy2') reccomb_names;
    1.34 -    val case_names' = map (Sign.intern_const thy2') case_names;
    1.35 +    val reccomb_names' = map (Sign.full_name thy2') reccomb_names;
    1.36 +    val case_names' = map (Sign.full_name thy2') case_names;
    1.37  
    1.38      val thy2 = thy2' |>
    1.39  
    1.40        (** size functions **)
    1.41  
    1.42 -      (if no_size then I else Theory.add_consts_i (map (fn (s, T) =>
    1.43 +      (if no_size then I else specify_consts (map (fn (s, T) =>
    1.44          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
    1.45            (size_names ~~ Library.drop (length (hd descr), recTs)))) |>
    1.46  
    1.47 @@ -650,7 +653,7 @@
    1.48        curry (Library.foldr (fn (((((_, (_, _, constrs)), T), tname),
    1.49          constr_syntax'), thy') => thy' |>
    1.50            add_path flat_names tname |>
    1.51 -            Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
    1.52 +            specify_consts (map (fn ((_, cargs), (cname, mx)) =>
    1.53                (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
    1.54                  (constrs ~~ constr_syntax')) |>
    1.55            parent_path flat_names))