--- a/src/Provers/splitter.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Provers/splitter.ML Sat Jan 21 23:02:14 2006 +0100
@@ -32,8 +32,8 @@
val delsplits : simpset * thm list -> simpset
val Addsplits : thm list -> unit
val Delsplits : thm list -> unit
- val split_add: Context.generic attribute
- val split_del: Context.generic attribute
+ val split_add: attribute
+ val split_del: attribute
val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
val setup: theory -> theory
end;
@@ -443,9 +443,9 @@
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
- Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
- Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
+ [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
+ Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
+ Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
fun split_meth src =
Method.syntax Attrib.local_thms src
@@ -456,8 +456,7 @@
val setup =
(Attrib.add_attributes
- [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
- "declaration of case split rule")] #>
+ [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
Method.add_methods [(splitN, split_meth, "apply case split rule")]);
end;