Method.modifier;

--- a/src/Provers/blast.ML	Wed Aug 18 20:45:52 1999 +0200
+++ b/src/Provers/blast.ML	Wed Aug 18 20:47:31 1999 +0200
@@ -67,7 +67,7 @@
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,
 		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
-  val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
+  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
   end;
 

--- a/src/Provers/clasimp.ML	Wed Aug 18 20:45:52 1999 +0200
+++ b/src/Provers/clasimp.ML	Wed Aug 18 20:47:31 1999 +0200
@@ -169,8 +169,8 @@
  [Method.add_methods
    [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp (improper!)"),
     ("auto", clasimp_method auto_tac, "auto"),
-    ("force", clasimp_method' force_tac, "force"),
-    ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];
+    ("force", clasimp_method' force_tac, "force")]];
+    
 
 
 end;

--- a/src/Provers/classical.ML	Wed Aug 18 20:45:52 1999 +0200
+++ b/src/Provers/classical.ML	Wed Aug 18 20:47:31 1999 +0200
@@ -171,7 +171,7 @@
   val xtra_elim_local: Proof.context attribute
   val xtra_intro_local: Proof.context attribute
   val delrule_local: Proof.context attribute
-  val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
+  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
   val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
@@ -1177,16 +1177,16 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- bbang >> K xtra_dest_local,
-  Args.$$$ destN -- bang >> K haz_dest_local,
-  Args.$$$ destN >> K safe_dest_local,
-  Args.$$$ elimN -- bbang >> K xtra_elim_local,
-  Args.$$$ elimN -- bang >> K haz_elim_local,
-  Args.$$$ elimN >> K safe_elim_local,
-  Args.$$$ introN -- bbang >> K xtra_intro_local,
-  Args.$$$ introN -- bang >> K haz_intro_local,
-  Args.$$$ introN >> K safe_intro_local,
-  Args.$$$ delN >> K delrule_local];
+ [Args.$$$ destN -- bbang >> K ((I, xtra_dest_local):Method.modifier),
+  Args.$$$ destN -- bang >> K (I, haz_dest_local),
+  Args.$$$ destN >> K (I, safe_dest_local),
+  Args.$$$ elimN -- bbang >> K (I, xtra_elim_local),
+  Args.$$$ elimN -- bang >> K (I, haz_elim_local),
+  Args.$$$ elimN >> K (I, safe_elim_local),
+  Args.$$$ introN -- bbang >> K (I, xtra_intro_local),
+  Args.$$$ introN -- bang >> K (I, haz_intro_local),
+  Args.$$$ introN >> K (I, safe_intro_local),
+  Args.$$$ delN >> K (I, delrule_local)];
 
 val cla_args = Method.only_sectioned_args cla_modifiers;