1.1 --- a/src/Pure/Isar/method.ML	Wed Aug 09 21:00:22 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 09 21:02:21 2000 +0200
     1.3 @@ -348,14 +348,17 @@
     1.4  (* res_inst_tac etc. *)
     1.5  
     1.6  (*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
     1.7 -fun gen_res_inst tac (quant, (insts, thm)) =
     1.8 -  METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm)));
     1.9 +fun gen_res_inst _ tac (quant, ([], thms)) =
    1.10 +      METHOD (fn facts => (quant (insert_tac facts THEN' tac thms)))
    1.11 +  | gen_res_inst tac _ (quant, (insts, [thm])) =
    1.12 +      METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm)))
    1.13 +  | gen_res_inst _ _ _ = error "Cannot have instantiations with multiple rules";
    1.14  
    1.15 -val res_inst = gen_res_inst Tactic.res_inst_tac;
    1.16 -val eres_inst = gen_res_inst Tactic.eres_inst_tac;
    1.17 -val dres_inst = gen_res_inst Tactic.dres_inst_tac;
    1.18 -val forw_inst = gen_res_inst Tactic.forw_inst_tac;
    1.19 -val cut_inst = gen_res_inst Tactic.cut_inst_tac;
    1.20 +val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac;
    1.21 +val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
    1.22 +val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
    1.23 +val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
    1.24 +val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_facts_tac;
    1.25  
    1.26  
    1.27  (* simple Prolog interpreter *)
    1.28 @@ -374,7 +377,8 @@
    1.29  fun tactic txt ctxt = METHOD (fn facts =>
    1.30   (Context.use_mltext
    1.31     ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
    1.32 -    \let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n"
    1.33 +    \let val thm = PureIsar.ProofContext.get_thm_closure ctxt\n\
    1.34 +    \  and thms = PureIsar.ProofContext.get_thms_closure ctxt in\n"
    1.35      ^ txt ^
    1.36      "\nend in PureIsar.Method.set_tactic tactic end")
    1.37    false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));
    1.38 @@ -510,8 +514,8 @@
    1.39  
    1.40  val insts =
    1.41    Scan.optional
    1.42 -    (Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --|
    1.43 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thm;
    1.44 +    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    1.45 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
    1.46  
    1.47  fun inst_args f = f oo (#2 oo syntax (Args.goal_spec HEADGOAL -- insts));
    1.48  
    1.49 @@ -633,9 +637,9 @@
    1.50    ("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"),
    1.51    ("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"),
    1.52    ("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
    1.53 -  ("subgoal_tac", subgoal_meth, "subgoal_tac emulation (dynamic instantiation!)"),
    1.54 -  ("thin_tac", thin_meth, "thin_tac emulation (dynamic instantiation!)"),
    1.55 -  ("rename_tac", rename_meth, "rename_tac emulation (dynamic instantiation!)"),
    1.56 +  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"),
    1.57 +  ("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"),
    1.58 +  ("rename_tac", rename_meth, "rename parameters (dynamic instantiation!)"),
    1.59    ("prolog", thms_args prolog, "simple prolog interpreter"),
    1.60    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
    1.61