AxClass.axiomatize_arity_i;
authorwenzelm
Sun Apr 30 22:50:03 2006 +0200 (2006-04-30)
changeset 1951029fc4e5a638c
parent 19509 351e1b1ea251
child 19511 b4bd790f9373
AxClass.axiomatize_arity_i;
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/domain/extender.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Apr 30 22:50:01 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 30 22:50:03 2006 +0200
     1.3 @@ -308,8 +308,8 @@
     1.4      val thy1' = thy1 |>
     1.5        Theory.copy |>
     1.6        Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
     1.7 -      Theory.add_arities_i (map (fn s =>
     1.8 -        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
     1.9 +      fold (fn s => AxClass.axiomatize_arity_i
    1.10 +        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    1.11          Extraction.add_typeof_eqns_i ty_eqs;
    1.12      val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
    1.13        SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Sun Apr 30 22:50:01 2006 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Sun Apr 30 22:50:03 2006 +0200
     2.3 @@ -50,16 +50,15 @@
     2.4  
     2.5  (** type declarations **)
     2.6  
     2.7 +fun HOL_arity (raw_name, args, mx) thy =
     2.8 +  thy |> AxClass.axiomatize_arity_i
     2.9 +    (Sign.full_name thy (Syntax.type_name raw_name mx),
    2.10 +      replicate (length args) HOLogic.typeS, HOLogic.typeS);
    2.11 +
    2.12  fun add_typedecls decls thy =
    2.13 -  let
    2.14 -    fun arity_of (raw_name, args, mx) =
    2.15 -      (Sign.full_name thy (Syntax.type_name raw_name mx),
    2.16 -        replicate (length args) HOLogic.typeS, HOLogic.typeS);
    2.17 -  in
    2.18 -    thy
    2.19 -    |> Theory.add_typedecls decls
    2.20 -    |> can (Theory.assert_super HOL.thy) ? Theory.add_arities_i (map arity_of decls)
    2.21 -  end;
    2.22 +  thy
    2.23 +  |> Theory.add_typedecls decls
    2.24 +  |> can (Theory.assert_super HOL.thy) ? fold HOL_arity decls;
    2.25  
    2.26  
    2.27  
     3.1 --- a/src/HOLCF/domain/extender.ML	Sun Apr 30 22:50:01 2006 +0200
     3.2 +++ b/src/HOLCF/domain/extender.ML	Sun Apr 30 22:50:03 2006 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4      fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
     3.5      fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     3.6      val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
     3.7 -		       |> Theory.add_arities_i (map thy_arity dtnvs);
     3.8 +		       |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
     3.9      val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
    3.10      val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
    3.11      val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');