# HG changeset patch
# User wenzelm
# Date 947069413 -3600
# Node ID a7ee88ef2fa53e2551bed12c92426edcac9cb7cd
# Parent  80a3c30d088bb28dfd7aba02d680bea6935efb28
METHOD_CLASET': refer to *local* claset;

diff -r 80a3c30d088b -r a7ee88ef2fa5 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Jan 05 11:48:08 2000 +0100
+++ b/src/Provers/classical.ML	Wed Jan 05 11:50:13 2000 +0100
@@ -1056,8 +1056,8 @@
 
 (* METHOD_CLASET' *)
 
-fun METHOD_CLASET' tac =
-  Method.METHOD (FIRSTGOAL o (fn facts => CLASET' (fn cs => tac cs facts)));
+fun METHOD_CLASET' tac ctxt =
+  Method.METHOD (FIRSTGOAL o tac (get_local_claset ctxt));
 
 
 val trace_rules = ref false;
@@ -1159,11 +1159,11 @@
 (** setup_methods **)
 
 val setup_methods = Method.add_methods
- [("default", Method.thms_args rule, "apply some rule"),
-  ("rule", Method.thms_args rule, "apply some rule"),
+ [("default", Method.thms_ctxt_args rule, "apply some rule"),
+  ("rule", Method.thms_ctxt_args rule, "apply some rule"),
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
-  ("intro", Method.thms_args intro, "repeatedly apply introduction rules"),
-  ("elim", Method.thms_args elim, "repeatedly apply elimination rules"),
+  ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
+  ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
   ("safe_tac", cla_method safe_tac, "safe_tac (improper!)"),
   ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"),
   ("step_tac", cla_method' step_tac, "step_tac (improper!)"),