# HG changeset patch
# User wenzelm
# Date 949057926 -3600
# Node ID dab09e1ad59447d5bcf64506219dee8553e9e3d8
# Parent  9bdbcb71dc561f28c9a4bce85aea5b72c72a2475
replaced FIRSTGOAL by FINDGOAL (backtracking!);

diff -r 9bdbcb71dc56 -r dab09e1ad594 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -72,7 +72,7 @@
 
 fun induct ctxt =
   Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name))
-  >> (fn (is, k) => Method.METHOD (FIRSTGOAL o induct_tac (ProofContext.theory_of ctxt) is k));
+  >> (fn (is, k) => Method.METHOD (FINDGOAL o induct_tac (ProofContext.theory_of ctxt) is k));
 
 fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src);
 val induct_method = ("induct", induct_meth, "induction on types, sets, functions etc.");
diff -r 9bdbcb71dc56 -r dab09e1ad594 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -520,7 +520,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (FIRSTGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)),
     "split record fields");
 
 
diff -r 9bdbcb71dc56 -r dab09e1ad594 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -158,7 +158,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
diff -r 9bdbcb71dc56 -r dab09e1ad594 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/classical.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -1057,7 +1057,7 @@
 (* METHOD_CLASET' *)
 
 fun METHOD_CLASET' tac ctxt =
-  Method.METHOD (FIRSTGOAL o tac (get_local_claset ctxt));
+  Method.METHOD (FINDGOAL o tac (get_local_claset ctxt));
 
 
 val trace_rules = ref false;
@@ -1149,7 +1149,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
 
 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
+  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
 
 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
diff -r 9bdbcb71dc56 -r dab09e1ad594 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -487,7 +487,7 @@
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
+    FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   |> Method.bang_sectioned_args simp_modifiers';