--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 13 23:13:10 2000 +0200
@@ -262,7 +262,7 @@
Theory.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
- (PureThy.add_defs_i o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+ (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
@@ -344,7 +344,7 @@
list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
val (thy', [def_thm]) = thy |>
- Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
+ Theory.add_consts_i [decl] |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
in (defs @ [def_thm], thy')
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
@@ -446,7 +446,7 @@
Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
(drop (length (hd descr), size_names ~~ recTs))) |>
- (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
+ (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
(def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
(size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>>
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 13 23:13:10 2000 +0200
@@ -233,7 +233,7 @@
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val (thy', [def_thm]) = thy |>
Theory.add_consts_i [(cname', constrT, mx)] |>
- (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
+ (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -381,7 +381,7 @@
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
- val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
+ val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
(* prove characteristic equations *)
--- a/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:13:10 2000 +0200
@@ -653,7 +653,7 @@
|> (if length cs < 2 then I
else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
|> Theory.add_path rec_name
- |> PureThy.add_defss_i [(("defs", def_terms), [])];
+ |> PureThy.add_defss_i false [(("defs", def_terms), [])];
val mono = prove_mono setT fp_fun monos thy'
--- a/src/HOL/Tools/primrec_package.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Jul 13 23:13:10 2000 +0200
@@ -296,7 +296,7 @@
val primrec_name =
if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
val (thy', defs_thms') = thy |> Theory.add_path primrec_name |>
- (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs'
+ (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive"));
val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms';
--- a/src/HOL/Tools/record_package.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/record_package.ML Thu Jul 13 23:13:10 2000 +0200
@@ -619,8 +619,8 @@
val (defs_thy, (field_defs, dest_defs)) =
types_thy
|> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
- |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) field_specs
- |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
+ |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) field_specs
+ |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
(* 3rd stage: thms_thy *)
@@ -789,9 +789,9 @@
|> Theory.add_trfuns ([], [], field_tr's, [])
|> (Theory.add_consts_i o map Syntax.no_syn)
(sel_decls @ update_decls @ make_decls)
- |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) sel_specs
- |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs
- |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
+ |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) sel_specs
+ |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) update_specs
+ |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;
(* 3rd stage: thms_thy *)
--- a/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:13:10 2000 +0200
@@ -141,7 +141,7 @@
((if no_def then [] else [(name, setT, NoSyn)]) @
[(Rep_name, newT --> oldT, NoSyn),
(Abs_name, oldT --> newT, NoSyn)])
- |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
+ |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
[Logic.mk_defpair (setC, set)])
|> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
[(Rep_name, rep_type),