--- 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),
--- 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
--- 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