--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 21 18:44:34 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 21 18:45:31 1999 +0200
@@ -260,7 +260,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)) |>
- Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
+ (PureThy.add_defs_i 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))))))
@@ -343,7 +343,7 @@
list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
val thy' = thy |>
- Theory.add_consts_i [decl] |> Theory.add_defs_i [def];
+ Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
in (defs @ [get_def thy' (Sign.base_name name)], thy')
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
@@ -446,13 +446,13 @@
Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
(drop (length (hd descr), size_names ~~ recTs))) |>
- Theory.add_defs_i (map (fn (((s, T), def_name), rec_name) =>
+ (PureThy.add_defs_i 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)) |>
parent_path flat_names;
- val size_def_thms = map (get_axiom thy') def_names;
+ val size_def_thms = map (get_thm thy') def_names;
val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
val size_thms = map (fn t => prove_goalw_cterm rewrites
--- a/src/HOL/Tools/datatype_package.ML Thu Oct 21 18:44:34 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML Thu Oct 21 18:45:31 1999 +0200
@@ -308,7 +308,7 @@
val thy'' = thy' |>
Theory.add_path tname |>
PureThy.add_axioms_i [((label, t), [])];
- val ax = get_axiom thy'' label
+ val ax = PureThy.get_thm thy'' label
in (Theory.parent_path thy'', ax::axs)
end) (tnames ~~ ts, (thy, []));
@@ -434,7 +434,7 @@
Theory.parent_path |>
add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
- val induct = get_axiom thy3 "induct";
+ val induct = get_thm thy3 "induct";
val rec_thms = get_thms thy3 "recs";
val size_thms = if no_size then [] else get_thms thy3 "size";
val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 21 18:44:34 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 21 18:45:31 1999 +0200
@@ -233,9 +233,9 @@
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val thy' = thy |>
Theory.add_consts_i [(cname', constrT, mx)] |>
- Theory.add_defs_i [(def_name, def)];
+ (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
- in (thy', defs @ [get_axiom thy' def_name], eqns @ [eqn], i + 1)
+ in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
end;
(* constructor definitions for datatype *)
@@ -267,9 +267,9 @@
(* get axioms from theory *)
val newT_iso_axms = map (fn s =>
- (get_axiom thy4 ("Abs_" ^ s ^ "_inverse"),
- get_axiom thy4 ("Rep_" ^ s ^ "_inverse"),
- get_axiom thy4 ("Rep_" ^ s))) new_type_names;
+ (get_thm thy4 ("Abs_" ^ s ^ "_inverse"),
+ get_thm thy4 ("Rep_" ^ s ^ "_inverse"),
+ get_thm thy4 ("Rep_" ^ s))) new_type_names;
(*------------------------------------------------*)
(* prove additional theorems: *)
@@ -382,8 +382,8 @@
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' = Theory.add_defs_i defs thy;
- val def_thms = map (get_axiom thy') (map fst defs);
+ val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
+ val def_thms = map (get_thm thy') (map fst defs);
(* prove characteristic equations *)
--- a/src/HOL/Tools/primrec_package.ML Thu Oct 21 18:44:34 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Oct 21 18:45:31 1999 +0200
@@ -241,10 +241,10 @@
val thy' = thy |>
Theory.add_path (if alt_name = "" then (space_implode "_"
(map (Sign.base_name o #1) defs)) else alt_name) |>
- (if eq_set (names1, names2) then Theory.add_defs_i defs'
+ (if eq_set (names1, names2) then (PureThy.add_defs_i 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) @ (map (get_axiom thy' o fst) defs');
+ val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ (map (get_thm thy' o fst) defs');
val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;
--- a/src/ZF/Tools/primrec_package.ML Thu Oct 21 18:44:34 1999 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Oct 21 18:45:31 1999 +0200
@@ -168,8 +168,8 @@
foldr (process_eqn thy) (map snd recursion_eqns, None);
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns)
val thy' = thy |> Theory.add_path (Sign.base_name (#1 def))
- |> Theory.add_defs_i [def]
- val rewrites = get_axiom thy' (#1 def) ::
+ |> (PureThy.add_defs_i o map Thm.no_attributes) [def]
+ val rewrites = get_thm thy' (#1 def) ::
map mk_meta_eq (#rec_rewrites con_info)
val char_thms =
(if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)