# HG changeset patch
# User wenzelm
# Date 933335006 -7200
# Node ID 5c31d06ead04e1b75506988e58f9927d8b949b6a
# Parent  0b2fe9ec709cdafa8e0ad5120fcc3b2bd36d6517
eliminated METHOD0 in favour of same_tac;

diff -r 0b2fe9ec709c -r 5c31d06ead04 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Jul 30 13:42:57 1999 +0200
+++ b/src/Provers/clasimp.ML	Fri Jul 30 13:43:26 1999 +0200
@@ -154,8 +154,11 @@
 val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
 val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
 
-fun clasimp_meth tac ctxt = Method.METHOD0 (tac (get_local_clasimpset ctxt));
-fun clasimp_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_clasimpset ctxt)));
+fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
+  ALLGOALS (Method.same_tac facts) THEN tac (get_local_clasimpset ctxt));
+
+fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
+  FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_clasimpset ctxt)));
 
 val clasimp_method = clasimp_args o clasimp_meth;
 val clasimp_method' = clasimp_args o clasimp_meth';
diff -r 0b2fe9ec709c -r 5c31d06ead04 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jul 30 13:42:57 1999 +0200
+++ b/src/Provers/classical.ML	Fri Jul 30 13:43:26 1999 +0200
@@ -1148,8 +1148,8 @@
 
 (* contradiction *)
 
-val contradiction =
-  Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
+val contradiction = Method.METHOD (fn facts =>
+  FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
 
 
 (* automatic methods *)
@@ -1168,8 +1168,11 @@
 
 val cla_args = Method.only_sectioned_args cla_modifiers;
 
-fun cla_meth tac ctxt = Method.METHOD0 (tac (get_local_claset ctxt));
-fun cla_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_claset ctxt)));
+fun cla_meth tac ctxt = Method.METHOD (fn facts =>
+  ALLGOALS (Method.same_tac facts) THEN tac (get_local_claset ctxt));
+
+fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
+  FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_claset ctxt)));
 
 val cla_method = cla_args o cla_meth;
 val cla_method' = cla_args o cla_meth';
@@ -1182,9 +1185,9 @@
  [("single", Method.no_args single, "apply standard rule (single step)"),
   ("default", Method.no_args single, "apply standard rule (single step)"),
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
-  ("safe_tac", cla_method safe_tac, "safe_tac"),
-  ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac"),
-  ("step_tac", cla_method' step_tac, "step_tac"),
+  ("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!)"),
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),
   ("slow", cla_method' slow_tac, "classical prover (depth-first, more backtracking)"),
diff -r 0b2fe9ec709c -r 5c31d06ead04 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jul 30 13:42:57 1999 +0200
+++ b/src/Provers/simplifier.ML	Fri Jul 30 13:43:26 1999 +0200
@@ -477,11 +477,11 @@
  [(simpN,               simp_method true true asm_full_simp_tac, "simplification"),
   (asm_simpN,           simp_method false true asm_full_simp_tac,
     "simplification (including assumption)"),
-  ("simp_tac",          simp_method false false simp_tac, "simp_tac"),
-  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac"),
-  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac"),
-  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac"),
-  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac")];
+  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
+  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
+  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
+  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
+  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];