src/Pure/drule.ML
changeset 52467 24c6ddb48cb8
parent 52465 4970437fe092
child 56245 84fc7dfa3cd4
--- a/src/Pure/drule.ML	Thu Jun 27 12:34:58 2013 +0200
+++ b/src/Pure/drule.ML	Thu Jun 27 17:06:22 2013 +0200
@@ -68,8 +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 compose: thm * int * thm -> thm
   val equals_cong: thm
   val imp_cong: thm
   val swap_prems_eq: thm
@@ -358,15 +357,10 @@
 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)
-fun compose(tha,i,thb) =
-  distinct Thm.eq_thm
-    (Seq.list_of
-      (Thm.bicompose {flatten = true, match = false, incremented = 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]));
+fun compose (tha, i, thb) =
+  Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
+  |> Seq.list_of |> distinct Thm.eq_thm
+  |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
 
 
 (** theorem equality **)