method parser: pass proper context;
authorwenzelm
Mon Mar 16 19:40:03 2009 +0100 (2009-03-16)
changeset 3055124e156db414c
parent 30550 c601204b055c
child 30552 58db56278478
child 30561 5e6088e1d6df
method parser: pass proper context;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Mar 16 18:24:39 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Mar 16 19:40:03 2009 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4    val subgoal_tac: Proof.context -> string -> int -> tactic
     1.5    val subgoals_tac: Proof.context -> string list -> int -> tactic
     1.6    val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     1.7 -    (thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
     1.8 +    (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
     1.9  end;
    1.10  
    1.11  signature RULE_INSTS =
    1.12 @@ -391,17 +391,17 @@
    1.13      (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
    1.14    Attrib.thms >>
    1.15    (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
    1.16 -    if null insts then quant (Method.insert_tac facts THEN' tac thms)
    1.17 +    if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
    1.18      else
    1.19        (case thms of
    1.20          [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
    1.21        | _ => error "Cannot have instantiations with multiple rules")));
    1.22  
    1.23 -val res_inst_meth = method res_inst_tac Tactic.resolve_tac;
    1.24 -val eres_inst_meth = method eres_inst_tac Tactic.eresolve_tac;
    1.25 -val cut_inst_meth = method cut_inst_tac Tactic.cut_rules_tac;
    1.26 -val dres_inst_meth = method dres_inst_tac Tactic.dresolve_tac;
    1.27 -val forw_inst_meth = method forw_inst_tac Tactic.forward_tac;
    1.28 +val res_inst_meth = method res_inst_tac (K Tactic.resolve_tac);
    1.29 +val eres_inst_meth = method eres_inst_tac (K Tactic.eresolve_tac);
    1.30 +val cut_inst_meth = method cut_inst_tac (K Tactic.cut_rules_tac);
    1.31 +val dres_inst_meth = method dres_inst_tac (K Tactic.dresolve_tac);
    1.32 +val forw_inst_meth = method forw_inst_tac (K Tactic.forward_tac);
    1.33  
    1.34  
    1.35  (* setup *)