# HG changeset patch
# User wenzelm
# Date 931532094 -7200
# Node ID 309276732ee1be1ea10311dc2451906ef7e7041e
# Parent  eeeef70c8fe3c41170c497e7ff7bf9a6a6a0c882
added compose_single;

diff -r eeeef70c8fe3 -r 309276732ee1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jul 09 16:45:18 1999 +0200
+++ b/src/Pure/drule.ML	Fri Jul 09 16:54:54 1999 +0200
@@ -81,6 +81,7 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val compose_single	: thm * int * thm -> thm
   val triv_goal		: thm
   val rev_triv_goal	: thm
   val mk_triv_goal      : cterm -> thm
@@ -348,6 +349,11 @@
 fun compose(tha,i,thb) =
     Seq.list_of (bicompose false (false,tha,0) i thb);
 
+fun compose_single (tha,i,thb) =
+  (case compose (tha,i,thb) of
+    [th] => th
+  | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
+
 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
 fun tha COMP thb =
     case compose(tha,1,thb) of