adapted PureThy.add_defs_i;
authorwenzelm
Thu Jul 13 23:13:10 2000 +0200 (2000-07-13)
changeset 9315f793f05024f6
parent 9314 fd8b0f219879
child 9316 e58778cc4d22
adapted PureThy.add_defs_i;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 13 23:11:38 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 13 23:13:10 2000 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4        Theory.add_consts_i (map (fn ((name, T), T') =>
     1.5          (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
     1.6            (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
     1.7 -      (PureThy.add_defs_i o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     1.8 +      (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     1.9          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    1.10             Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.11               HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
    1.12 @@ -344,7 +344,7 @@
    1.13                list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
    1.14                  fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
    1.15            val (thy', [def_thm]) = thy |>
    1.16 -            Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
    1.17 +            Theory.add_consts_i [decl] |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
    1.18  
    1.19          in (defs @ [def_thm], thy')
    1.20          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    1.21 @@ -446,7 +446,7 @@
    1.22        Theory.add_consts_i (map (fn (s, T) =>
    1.23          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
    1.24            (drop (length (hd descr), size_names ~~ recTs))) |>
    1.25 -      (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
    1.26 +      (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
    1.27          (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
    1.28            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
    1.29              (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>>
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 13 23:11:38 2000 +0200
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 13 23:13:10 2000 +0200
     2.3 @@ -233,7 +233,7 @@
     2.4            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
     2.5          val (thy', [def_thm]) = thy |>
     2.6            Theory.add_consts_i [(cname', constrT, mx)] |>
     2.7 -          (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
     2.8 +          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
     2.9  
    2.10        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    2.11  
    2.12 @@ -381,7 +381,7 @@
    2.13          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    2.14            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    2.15              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    2.16 -        val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    2.17 +        val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
    2.18  
    2.19          (* prove characteristic equations *)
    2.20  
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jul 13 23:11:38 2000 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 13 23:13:10 2000 +0200
     3.3 @@ -653,7 +653,7 @@
     3.4        |> (if length cs < 2 then I
     3.5            else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
     3.6        |> Theory.add_path rec_name
     3.7 -      |> PureThy.add_defss_i [(("defs", def_terms), [])];
     3.8 +      |> PureThy.add_defss_i false [(("defs", def_terms), [])];
     3.9  
    3.10      val mono = prove_mono setT fp_fun monos thy'
    3.11  
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Jul 13 23:11:38 2000 +0200
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Jul 13 23:13:10 2000 +0200
     4.3 @@ -296,7 +296,7 @@
     4.4      val primrec_name =
     4.5        if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
     4.6      val (thy', defs_thms') = thy |> Theory.add_path primrec_name |>
     4.7 -      (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs'
     4.8 +      (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
     4.9         else primrec_err ("functions " ^ commas_quote names2 ^
    4.10           "\nare not mutually recursive"));
    4.11      val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms';
     5.1 --- a/src/HOL/Tools/record_package.ML	Thu Jul 13 23:11:38 2000 +0200
     5.2 +++ b/src/HOL/Tools/record_package.ML	Thu Jul 13 23:13:10 2000 +0200
     5.3 @@ -619,8 +619,8 @@
     5.4      val (defs_thy, (field_defs, dest_defs)) =
     5.5        types_thy
     5.6         |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
     5.7 -       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) field_specs
     5.8 -       |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
     5.9 +       |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) field_specs
    5.10 +       |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
    5.11  
    5.12  
    5.13      (* 3rd stage: thms_thy *)
    5.14 @@ -789,9 +789,9 @@
    5.15        |> Theory.add_trfuns ([], [], field_tr's, [])
    5.16        |> (Theory.add_consts_i o map Syntax.no_syn)
    5.17          (sel_decls @ update_decls @ make_decls)
    5.18 -      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) sel_specs
    5.19 -      |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs
    5.20 -      |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
    5.21 +      |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) sel_specs
    5.22 +      |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) update_specs
    5.23 +      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;
    5.24  
    5.25  
    5.26      (* 3rd stage: thms_thy *)
     6.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jul 13 23:11:38 2000 +0200
     6.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 13 23:13:10 2000 +0200
     6.3 @@ -141,7 +141,7 @@
     6.4         ((if no_def then [] else [(name, setT, NoSyn)]) @
     6.5          [(Rep_name, newT --> oldT, NoSyn),
     6.6           (Abs_name, oldT --> newT, NoSyn)])
     6.7 -      |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
     6.8 +      |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
     6.9         [Logic.mk_defpair (setC, set)])
    6.10        |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
    6.11         [(Rep_name, rep_type),