src/Pure/Isar/method.ML
changeset 10309 a7f961fb62c6
parent 10034 4bca6b2d2589
child 10378 98c95ebf804f
     1.1 --- a/src/Pure/Isar/method.ML	Mon Oct 23 22:09:52 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Oct 23 22:10:36 2000 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4      -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
     1.5    val rule_tac: thm list -> thm list -> int -> tactic
     1.6    val erule_tac: thm list -> thm list -> int -> tactic
     1.7 +  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
     1.8    val rule: thm list -> Proof.method
     1.9    val erule: thm list -> Proof.method
    1.10    val drule: thm list -> Proof.method
    1.11 @@ -323,14 +324,15 @@
    1.12  fun gen_rule_tac tac rules [] = tac rules
    1.13    | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
    1.14  
    1.15 -fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
    1.16 -
    1.17 -fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
    1.18 +fun gen_some_rule_tac tac arg_rules ctxt facts =
    1.19    let val rules =
    1.20      if not (null arg_rules) then arg_rules
    1.21      else if null facts then #1 (LocalRules.get ctxt)
    1.22      else op @ (LocalRules.get ctxt);
    1.23 -  in HEADGOAL (tac rules facts) end);
    1.24 +  in tac rules facts end;
    1.25 +
    1.26 +fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
    1.27 +fun gen_rule' tac arg_rules ctxt = METHOD (HEADGOAL o gen_some_rule_tac tac arg_rules ctxt);
    1.28  
    1.29  fun setup raw_tac =
    1.30    let val tac = gen_rule_tac raw_tac
    1.31 @@ -338,6 +340,7 @@
    1.32  
    1.33  in
    1.34  
    1.35 +val some_rule_tac = gen_some_rule_tac (gen_rule_tac Tactic.resolve_tac);
    1.36  val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac;
    1.37  val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac;
    1.38  val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac;
    1.39 @@ -648,7 +651,6 @@
    1.40    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    1.41    ("unfold", thms_args unfold, "unfold definitions"),
    1.42    ("fold", thms_args fold, "fold definitions"),
    1.43 -  ("default", thms_ctxt_args some_rule, "apply some rule"),
    1.44    ("rule", thms_ctxt_args some_rule, "apply some rule"),
    1.45    ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper)"),
    1.46    ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper)"),