HEADGOAL;
authorwenzelm
Wed Apr 05 21:02:31 2000 +0200 (2000-04-05)
changeset 86716ce91a80f616
parent 8670 d69616c74211
child 8672 1f51c411da5a
HEADGOAL;
src/HOL/Tools/induct_method.ML
src/Provers/classical.ML
src/Pure/Isar/method.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Wed Apr 05 21:02:19 2000 +0200
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Wed Apr 05 21:02:31 2000 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val cases_meth = Method.METHOD_CASES o (FINDGOAL oo cases_tac);
     1.8 +val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -333,7 +333,7 @@
    1.13  
    1.14  in
    1.15  
    1.16 -val induct_meth = Method.METHOD_CASES o (FINDGOAL oo induct_tac);
    1.17 +val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
    1.18  
    1.19  end;
    1.20  
     2.1 --- a/src/Provers/classical.ML	Wed Apr 05 21:02:19 2000 +0200
     2.2 +++ b/src/Provers/classical.ML	Wed Apr 05 21:02:31 2000 +0200
     2.3 @@ -1060,7 +1060,7 @@
     2.4  (* METHOD_CLASET' *)
     2.5  
     2.6  fun METHOD_CLASET' tac ctxt =
     2.7 -  Method.METHOD (FINDGOAL o tac (get_local_claset ctxt));
     2.8 +  Method.METHOD (HEADGOAL o tac (get_local_claset ctxt));
     2.9  
    2.10  
    2.11  val trace_rules = ref false;
     3.1 --- a/src/Pure/Isar/method.ML	Wed Apr 05 21:02:19 2000 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 05 21:02:31 2000 +0200
     3.3 @@ -279,14 +279,14 @@
     3.4  fun gen_rule_tac tac rules [] = tac rules
     3.5    | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
     3.6  
     3.7 -fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);
     3.8 +fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
     3.9  
    3.10  fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
    3.11    let val rules =
    3.12      if not (null arg_rules) then arg_rules
    3.13      else if null facts then #1 (LocalRules.get ctxt)
    3.14      else op @ (LocalRules.get ctxt);
    3.15 -  in FINDGOAL (tac rules facts) end);
    3.16 +  in HEADGOAL (tac rules facts) end);
    3.17  
    3.18  fun setup raw_tac =
    3.19    let val tac = gen_rule_tac raw_tac
    3.20 @@ -304,7 +304,7 @@
    3.21  
    3.22  (* this *)
    3.23  
    3.24 -val this = METHOD (EVERY o map (FINDGOAL o Tactic.rtac));
    3.25 +val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
    3.26  
    3.27  
    3.28  (* assumption *)
    3.29 @@ -316,7 +316,7 @@
    3.30    | assumption_tac _ [fact] = resolve_tac [fact]
    3.31    | assumption_tac _ _ = K no_tac;
    3.32  
    3.33 -fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
    3.34 +fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);
    3.35  
    3.36  
    3.37  (* res_inst_tac emulations *)
    3.38 @@ -346,7 +346,7 @@
    3.39  
    3.40  fun tactic txt ctxt = METHOD (fn facts =>
    3.41   (Context.use_mltext
    3.42 -   ("let fun (tactic: PureIsar.Proof.context -> thm list -> tactic) ctxt facts = \
    3.43 +   ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
    3.44      \let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n"
    3.45      ^ txt ^
    3.46      "\nend in PureIsar.Method.set_tactic tactic end")
     4.1 --- a/src/Pure/axclass.ML	Wed Apr 05 21:02:19 2000 +0200
     4.2 +++ b/src/Pure/axclass.ML	Wed Apr 05 21:02:31 2000 +0200
     4.3 @@ -306,7 +306,7 @@
     4.4  (* intro_classes *)
     4.5  
     4.6  fun intro_classes_tac facts st =
     4.7 -  FINDGOAL (Method.insert_tac facts THEN'
     4.8 +  HEADGOAL (Method.insert_tac facts THEN'
     4.9        REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
    4.10  
    4.11  val intro_classes_method =