1.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Sep 18 11:08:28 2013 +0200
     1.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Sep 18 11:36:12 2013 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Tools/rule_insts.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Rule instantiations -- operations within a rule/subgoal context.
     1.8 +Rule instantiations -- operations within implicit rule / subgoal context.
     1.9  *)
    1.10  
    1.11  signature BASIC_RULE_INSTS =
    1.12 @@ -15,14 +15,14 @@
    1.13    val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.14    val thin_tac: Proof.context -> string -> int -> tactic
    1.15    val subgoal_tac: Proof.context -> string -> int -> tactic
    1.16 -  val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
    1.17 -    (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.18  end;
    1.19  
    1.20  signature RULE_INSTS =
    1.21  sig
    1.22    include BASIC_RULE_INSTS
    1.23    val make_elim_preserve: thm -> thm
    1.24 +  val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
    1.25 +    (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.26  end;
    1.27  
    1.28  structure Rule_Insts: RULE_INSTS =
    1.29 @@ -164,7 +164,7 @@
    1.30  (* where: named instantiation *)
    1.31  
    1.32  val _ = Theory.setup
    1.33 -  (Attrib.setup (Binding.name "where")
    1.34 +  (Attrib.setup @{binding "where"}
    1.35      (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
    1.36        (fn args =>
    1.37          Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
    1.38 @@ -185,7 +185,7 @@
    1.39  in
    1.40  
    1.41  val _ = Theory.setup
    1.42 -  (Attrib.setup (Binding.name "of")
    1.43 +  (Attrib.setup @{binding "of"}
    1.44      (Scan.lift insts >> (fn args =>
    1.45        Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
    1.46      "positional instantiation of theorem");
    1.47 @@ -315,9 +315,7 @@
    1.48  
    1.49  
    1.50  
    1.51 -(** methods **)
    1.52 -
    1.53 -(* rule_tac etc. -- refer to dynamic goal state! *)
    1.54 +(* method wrapper *)
    1.55  
    1.56  fun method inst_tac tac =
    1.57    Args.goal_spec --
    1.58 @@ -332,30 +330,28 @@
    1.59          [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
    1.60        | _ => error "Cannot have instantiations with multiple rules")));
    1.61  
    1.62 -val res_inst_meth = method res_inst_tac (K resolve_tac);
    1.63 -val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
    1.64 -val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
    1.65 -val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
    1.66 -val forw_inst_meth = method forw_inst_tac (K forward_tac);
    1.67 -
    1.68  
    1.69  (* setup *)
    1.70  
    1.71 +(*warning: rule_tac etc. refer to dynamic subgoal context!*)
    1.72 +
    1.73  val _ = Theory.setup
    1.74 - (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
    1.75 -  Method.setup (Binding.name "erule_tac") eres_inst_meth
    1.76 + (Method.setup @{binding rule_tac} (method res_inst_tac (K resolve_tac))
    1.77 +    "apply rule (dynamic instantiation)" #>
    1.78 +  Method.setup @{binding erule_tac} (method eres_inst_tac (K eresolve_tac))
    1.79      "apply rule in elimination manner (dynamic instantiation)" #>
    1.80 -  Method.setup (Binding.name "drule_tac") dres_inst_meth
    1.81 +  Method.setup @{binding drule_tac} (method dres_inst_tac (K dresolve_tac))
    1.82      "apply rule in destruct manner (dynamic instantiation)" #>
    1.83 -  Method.setup (Binding.name "frule_tac") forw_inst_meth
    1.84 +  Method.setup @{binding frule_tac} (method forw_inst_tac (K forward_tac))
    1.85      "apply rule in forward manner (dynamic instantiation)" #>
    1.86 -  Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
    1.87 -  Method.setup (Binding.name "subgoal_tac")
    1.88 +  Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
    1.89 +    "cut rule (dynamic instantiation)" #>
    1.90 +  Method.setup @{binding subgoal_tac}
    1.91      (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
    1.92        (fn (quant, props) => fn ctxt =>
    1.93          SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
    1.94      "insert subgoal (dynamic instantiation)" #>
    1.95 -  Method.setup (Binding.name "thin_tac")
    1.96 +  Method.setup @{binding thin_tac}
    1.97      (Args.goal_spec -- Scan.lift Args.name_source >>
    1.98        (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
    1.99        "remove premise (dynamic instantiation)");