src/Provers/splitter.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18988 d6e5fa2ba8b8
     1.1 --- a/src/Provers/splitter.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Provers/splitter.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -32,8 +32,8 @@
     1.4    val delsplits       : simpset * thm list -> simpset
     1.5    val Addsplits       : thm list -> unit
     1.6    val Delsplits       : thm list -> unit
     1.7 -  val split_add: Context.generic attribute
     1.8 -  val split_del: Context.generic attribute
     1.9 +  val split_add: attribute
    1.10 +  val split_del: attribute
    1.11    val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
    1.12    val setup: theory -> theory
    1.13  end;
    1.14 @@ -443,9 +443,9 @@
    1.15  (* methods *)
    1.16  
    1.17  val split_modifiers =
    1.18 - [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
    1.19 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
    1.20 -  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
    1.21 + [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
    1.22 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
    1.23 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
    1.24  
    1.25  fun split_meth src =
    1.26    Method.syntax Attrib.local_thms src
    1.27 @@ -456,8 +456,7 @@
    1.28  
    1.29  val setup =
    1.30   (Attrib.add_attributes
    1.31 -  [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
    1.32 -    "declaration of case split rule")] #>
    1.33 +  [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
    1.34    Method.add_methods [(splitN, split_meth, "apply case split rule")]);
    1.35  
    1.36  end;