# HG changeset patch
# User wenzelm
# Date 954961351 -7200
# Node ID 6ce91a80f616757da0a8db239cef49a377043a36
# Parent  d69616c7421179a04624e50350b33217ab9bde01
HEADGOAL;

diff -r d69616c74211 -r 6ce91a80f616 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Wed Apr 05 21:02:19 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Wed Apr 05 21:02:31 2000 +0200
@@ -235,7 +235,7 @@
 
 in
 
-val cases_meth = Method.METHOD_CASES o (FINDGOAL oo cases_tac);
+val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
 
 end;
 
@@ -333,7 +333,7 @@
 
 in
 
-val induct_meth = Method.METHOD_CASES o (FINDGOAL oo induct_tac);
+val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
 
 end;
 
diff -r d69616c74211 -r 6ce91a80f616 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Apr 05 21:02:19 2000 +0200
+++ b/src/Provers/classical.ML	Wed Apr 05 21:02:31 2000 +0200
@@ -1060,7 +1060,7 @@
 (* METHOD_CLASET' *)
 
 fun METHOD_CLASET' tac ctxt =
-  Method.METHOD (FINDGOAL o tac (get_local_claset ctxt));
+  Method.METHOD (HEADGOAL o tac (get_local_claset ctxt));
 
 
 val trace_rules = ref false;
diff -r d69616c74211 -r 6ce91a80f616 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Apr 05 21:02:19 2000 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 05 21:02:31 2000 +0200
@@ -279,14 +279,14 @@
 fun gen_rule_tac tac rules [] = tac rules
   | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
 
-fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);
+fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
 
 fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
   let val rules =
     if not (null arg_rules) then arg_rules
     else if null facts then #1 (LocalRules.get ctxt)
     else op @ (LocalRules.get ctxt);
-  in FINDGOAL (tac rules facts) end);
+  in HEADGOAL (tac rules facts) end);
 
 fun setup raw_tac =
   let val tac = gen_rule_tac raw_tac
@@ -304,7 +304,7 @@
 
 (* this *)
 
-val this = METHOD (EVERY o map (FINDGOAL o Tactic.rtac));
+val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
 
 
 (* assumption *)
@@ -316,7 +316,7 @@
   | assumption_tac _ [fact] = resolve_tac [fact]
   | assumption_tac _ _ = K no_tac;
 
-fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
+fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);
 
 
 (* res_inst_tac emulations *)
@@ -346,7 +346,7 @@
 
 fun tactic txt ctxt = METHOD (fn facts =>
  (Context.use_mltext
-   ("let fun (tactic: PureIsar.Proof.context -> thm list -> tactic) ctxt facts = \
+   ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
     \let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n"
     ^ txt ^
     "\nend in PureIsar.Method.set_tactic tactic end")
diff -r d69616c74211 -r 6ce91a80f616 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 05 21:02:19 2000 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 05 21:02:31 2000 +0200
@@ -306,7 +306,7 @@
 (* intro_classes *)
 
 fun intro_classes_tac facts st =
-  FINDGOAL (Method.insert_tac facts THEN'
+  HEADGOAL (Method.insert_tac facts THEN'
       REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
 
 val intro_classes_method =