# HG changeset patch
# User wenzelm
# Date 931287783 -7200
# Node ID 020314dadebd7d60452c6a7791fcb6d629773763
# Parent  2650bd68c0ba43eb8c3da6ffa5132fdd3712e6c8
added clear_mss;

diff -r 2650bd68c0ba -r 020314dadebd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jul 05 09:52:25 1999 +0200
+++ b/src/Pure/thm.ML	Tue Jul 06 21:03:03 1999 +0200
@@ -151,6 +151,7 @@
   val dest_mss		: meta_simpset ->
     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   val empty_mss         : meta_simpset
+  val clear_mss		: meta_simpset -> meta_simpset
   val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
   val add_simps         : meta_simpset * thm list -> meta_simpset
   val del_simps         : meta_simpset * thm list -> meta_simpset
@@ -1582,8 +1583,10 @@
 
 val empty_mss =
   let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
-  in mk_mss (Net.empty, ([],[]), Net.empty, [], [], mk_rews, Term.termless)
-  end;
+  in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless) end;
+
+fun clear_mss (Mss {mk_rews, termless, ...}) =
+  mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);