# HG changeset patch
# User wenzelm
# Date 1004042570 -7200
# Node ID 7b594aba130078fb5df2e2318d87952ee30f86e3
# Parent  2a2b1182a23b0fad5d483457d1dafa14bee8ef6b
'simplified' att: args;

diff -r 2a2b1182a23b -r 7b594aba1300 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Oct 25 22:42:12 2001 +0200
+++ b/src/Provers/simplifier.ML	Thu Oct 25 22:42:50 2001 +0200
@@ -488,13 +488,15 @@
     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
     Scan.succeed asm_full_simplify) |> Scan.lift) x;
 
-fun simplified_att get =
-  Attrib.syntax (conv_mode >> (fn f => Drule.rule_attribute (f o get)));
+fun simplified_att get args =
+  Attrib.syntax (conv_mode -- args >> (fn (f, ths) =>
+    Drule.rule_attribute (fn x => f ((if null ths then I else clear_ss) (get x) addsimps ths))));
 
 in
 
 val simplified_attr =
-  (simplified_att simpset_of, simplified_att get_local_simpset);
+ (simplified_att simpset_of Attrib.global_thmss,
+  simplified_att get_local_simpset Attrib.local_thmss);
 
 end;