--- a/src/Pure/Isar/rule_insts.ML Mon Mar 16 17:46:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Mon Mar 16 17:47:26 2009 +0100
@@ -16,6 +16,8 @@
val thin_tac: Proof.context -> string -> int -> tactic
val subgoal_tac: Proof.context -> string -> int -> tactic
val subgoals_tac: Proof.context -> string list -> int -> tactic
+ val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
+ (thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
signature RULE_INSTS =
@@ -383,9 +385,7 @@
(* rule_tac etc. -- refer to dynamic goal state! *)
-local
-
-fun inst_meth inst_tac tac =
+fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
(P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
@@ -397,15 +397,11 @@
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
| _ => error "Cannot have instantiations with multiple rules")));
-in
-
-val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
-val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
-val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
-val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
-val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
-
-end;
+val res_inst_meth = method res_inst_tac Tactic.resolve_tac;
+val eres_inst_meth = method eres_inst_tac Tactic.eresolve_tac;
+val cut_inst_meth = method cut_inst_tac Tactic.cut_rules_tac;
+val dres_inst_meth = method dres_inst_tac Tactic.dresolve_tac;
+val forw_inst_meth = method forw_inst_tac Tactic.forward_tac;
(* setup *)