--- a/TFL/tfl.sml Thu Jul 13 23:20:33 2000 +0200
+++ b/TFL/tfl.sml Thu Jul 13 23:20:57 2000 +0200
@@ -382,7 +382,7 @@
(wfrec $ map_term_types poly_tvars R)
$ functional
val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
- in #1 (PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy) end
+ in #1 (PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy) end
end;
@@ -537,7 +537,7 @@
(Name, Ty, S.list_mk_abs (args,rhs))
val (theory, [def0]) =
thy
- |> PureThy.add_defs_i
+ |> PureThy.add_defs_i false
[Thm.no_attributes (fid ^ "_def", defn)]
val def = freezeT def0;
val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
--- a/src/ZF/Tools/datatype_package.ML Thu Jul 13 23:20:33 2000 +0200
+++ b/src/ZF/Tools/datatype_package.ML Thu Jul 13 23:20:57 2000 +0200
@@ -245,14 +245,14 @@
if need_recursor then
thy |> Theory.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> (#1 o PureThy.add_defs_i [Thm.no_attributes recursor_def])
+ |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
else thy;
val (thy0, con_defs) = thy_path
|> Theory.add_consts_i
((case_base_name, case_typ, NoSyn) ::
map #1 (flat con_ty_lists))
- |> PureThy.add_defs_i
+ |> PureThy.add_defs_i false
(map Thm.no_attributes
(case_def ::
flat (ListPair.map mk_con_defs
--- a/src/ZF/Tools/inductive_package.ML Thu Jul 13 23:20:33 2000 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jul 13 23:20:57 2000 +0200
@@ -182,7 +182,7 @@
(*add definitions of the inductive sets*)
val thy1 = thy |> Theory.add_path big_rec_base_name
- |> (#1 o PureThy.add_defs_i (map Thm.no_attributes axpairs))
+ |> (#1 o PureThy.add_defs_i false (map Thm.no_attributes axpairs))
(*fetch fp definitions from the theory*)
--- a/src/ZF/Tools/primrec_package.ML Thu Jul 13 23:20:33 2000 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Jul 13 23:20:57 2000 +0200
@@ -169,7 +169,7 @@
foldr (process_eqn thy) (map snd recursion_eqns, None);
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns)
val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
- |> (PureThy.add_defs_i o map Thm.no_attributes) [def]
+ |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val char_thms =
(if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)