# HG changeset patch
# User wenzelm
# Date 1213478397 -7200
# Node ID 388fd72e9f265e619e53a73b19469554d60a1ca8
# Parent  5fe899199f85509bd1e4cb085f8f03ec26e10cd6
qualified old res_inst_tac variants;

diff -r 5fe899199f85 -r 388fd72e9f26 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 14 23:19:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 14 23:19:57 2008 +0200
@@ -307,26 +307,27 @@
 
   \item [@{method rule_tac} etc.] do resolution of rules with explicit
   instantiation.  This works the same way as the ML tactics @{ML
-  res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}).
+  Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
 
   Multiple rules may be only given if there is no instantiation; then
   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   \cite[\S3]{isabelle-ref}).
 
   \item [@{method cut_tac}] inserts facts into the proof state as
-  assumption of a subgoal, see also @{ML cut_facts_tac} in
+  assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
   \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
   variables is spread over the main goal statement.  Instantiations
-  may be given as well, see also ML tactic @{ML cut_inst_tac} in
-  \cite[\S3]{isabelle-ref}.
+  may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
+  in \cite[\S3]{isabelle-ref}.
 
   \item [@{method thin_tac}~@{text \<phi>}] deletes the specified
   assumption from a subgoal; note that @{text \<phi>} may contain schematic
-  variables.  See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
+  variables.  See also @{ML Tactic.thin_tac} in
+  \cite[\S3]{isabelle-ref}.
 
   \item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
-  assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
-  subgoals_tac} in \cite[\S3]{isabelle-ref}.
+  assumption to a subgoal.  See also @{ML Tactic.subgoal_tac} and @{ML
+  Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
 
   \item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
   parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
diff -r 5fe899199f85 -r 388fd72e9f26 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Jun 14 23:19:51 2008 +0200
+++ b/src/Pure/tactic.ML	Sat Jun 14 23:19:57 2008 +0200
@@ -39,19 +39,9 @@
   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
   val term_lift_inst_rule:
     thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
-  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
-  val res_inst_tac: (string * string) list -> thm -> int -> tactic
-  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
-  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
-  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
-  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
-  val instantiate_tac: (string * string) list -> tactic
-  val thin_tac: string -> int -> tactic
   val metacut_tac: thm -> int -> tactic
   val cut_rules_tac: thm list -> int -> tactic
   val cut_facts_tac: thm list -> int -> tactic
-  val subgoal_tac: string -> int -> tactic
-  val subgoals_tac: string list -> int -> tactic
   val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
   val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
     bool -> 'a Net.net * 'a Net.net -> int -> tactic
@@ -82,11 +72,21 @@
   include BASIC_TACTIC
   val innermost_params: int -> thm -> (string * typ) list
   val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
+  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
+  val res_inst_tac: (string * string) list -> thm -> int -> tactic
+  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
+  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
+  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
+  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
+  val instantiate_tac: (string * string) list -> tactic
   val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
   val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
   val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
   val make_elim_preserve: thm -> thm
   val instantiate_tac': (indexname * string) list -> tactic
+  val thin_tac: string -> int -> tactic
+  val subgoal_tac: string -> int -> tactic
+  val subgoals_tac: string list -> int -> tactic
   val untaglist: (int * 'a) list -> 'a list
   val orderlist: (int * 'a) list -> 'a list
   val insert_tagged_brl: 'a * (bool * thm) ->