# HG changeset patch
# User wenzelm
# Date 1372325622 -7200
# Node ID 4970437fe092bf4ab64c936ae26d4dda1b2bae42
# Parent  36497ee02ed8dd4b7bc2e19ea5184e5dd093dc21
tuned signature;

diff -r 36497ee02ed8 -r 4970437fe092 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 11:07:48 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 11:33:42 2013 +0200
@@ -491,7 +491,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
-  @{index_ML compose: "thm * int * thm -> thm list"} \\
+  @{index_ML Drule.compose: "thm * int * thm -> thm list"} \\
   @{index_ML_op COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
@@ -505,14 +505,14 @@
   performs elim-resolution --- it solves the first premise of @{text
   "rule"} by assumption and deletes that assumption.
 
-  \item @{ML compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
+  \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
   regarded as an atomic formula, to solve premise @{text "i"} of
   @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
   "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  For each @{text "s"} that unifies
   @{text "\<psi>"} and @{text "\<phi>"}, the result list contains the theorem
   @{text "(\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.
 
-  \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "compose (thm\<^sub>1, 1,
+  \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "Drule.compose (thm\<^sub>1, 1,
   thm\<^sub>2)"} and returns the result, if unique; otherwise, it raises
   exception @{ML THM}.
 
diff -r 36497ee02ed8 -r 4970437fe092 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 27 11:07:48 2013 +0200
+++ b/src/Pure/drule.ML	Thu Jun 27 11:33:42 2013 +0200
@@ -34,7 +34,6 @@
   val RL: thm list * thm list -> thm list
   val MRS: thm list * thm -> thm
   val OF: thm * thm list -> thm
-  val compose: thm * int * thm -> thm list
   val COMP: thm * thm -> thm
   val INCR_COMP: thm * thm -> thm
   val COMP_INCR: thm * thm -> thm
@@ -69,6 +68,7 @@
   val store_standard_thm_open: binding -> thm -> thm
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
+  val compose: thm * int * thm -> thm list
   val compose_single: thm * int * thm -> thm
   val equals_cong: thm
   val imp_cong: thm