# HG changeset patch
# User wenzelm
# Date 963523257 -7200
# Node ID d2655dc8a4b46103d49abc89b24fd5aaeaeaafc4
# Parent  1a46c94d14255b18b2006e7f43697cfc21945d71
adapted PureThy.add_defs_i;

diff -r 1a46c94d1425 -r d2655dc8a4b4 TFL/tfl.sml
--- 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)
diff -r 1a46c94d1425 -r d2655dc8a4b4 src/ZF/Tools/datatype_package.ML
--- 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
diff -r 1a46c94d1425 -r d2655dc8a4b4 src/ZF/Tools/inductive_package.ML
--- 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*)
diff -r 1a46c94d1425 -r d2655dc8a4b4 src/ZF/Tools/primrec_package.ML
--- 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 (!?) *)