# HG changeset patch
# User wenzelm
# Date 1136918007 -3600
# Node ID bdf01da93ed4967a487ec462ef8305948dc77872
# Parent  da46244359659d61337ac3594b0300577664680b
Attrib.rule;

diff -r da4624435965 -r bdf01da93ed4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Jan 10 15:23:31 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Jan 10 19:33:27 2006 +0100
@@ -491,7 +491,7 @@
 
 val skolem_global = Attrib.no_args skolem_global_fun;
 
-fun skolem_local x = Attrib.no_args (Drule.rule_attribute (K (conj_rule o skolem_thm))) x;
+fun skolem_local x = Attrib.no_args (Attrib.rule (K (conj_rule o skolem_thm))) x;
 
 val setup_attrs = Attrib.add_attributes
  [("skolem", (skolem_global, skolem_local),
diff -r da4624435965 -r bdf01da93ed4 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Tue Jan 10 15:23:31 2006 +0100
+++ b/src/HOL/Tools/split_rule.ML	Tue Jan 10 19:33:27 2006 +0100
@@ -136,9 +136,9 @@
 
 fun split_format x = Attrib.syntax
   (Scan.lift (Args.parens (Args.$$$ "complete"))
-    >> K (Drule.rule_attribute (K complete_split_rule)) ||
+    >> K (Attrib.rule (K complete_split_rule)) ||
   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
-    >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
+    >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
 
 val setup =
  [Attrib.add_attributes
diff -r da4624435965 -r bdf01da93ed4 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Jan 10 15:23:31 2006 +0100
+++ b/src/Pure/simplifier.ML	Tue Jan 10 19:33:27 2006 +0100
@@ -263,9 +263,8 @@
     Scan.succeed asm_full_simplify) |> Scan.lift) x;
 
 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 MetaSimplifier.clear_ss) (get x) addsimps ths))));
+  Attrib.syntax (conv_mode -- args >> (fn (f, ths) => Attrib.rule (fn x =>
+    f ((if null ths then I else MetaSimplifier.clear_ss) (get x) addsimps ths))));
 
 in