# HG changeset patch
# User wenzelm
# Date 1135347406 -3600
# Node ID 7569674d7bb1914be44d5b2a68e305eb8c290c11
# Parent  ef36f9be255edb08f40326e73015937a56d4ada9
Thm.compose_no_flatten;

diff -r ef36f9be255e -r 7569674d7bb1 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Dec 23 15:16:44 2005 +0100
+++ b/src/Pure/goal.ML	Fri Dec 23 15:16:46 2005 +0100
@@ -52,7 +52,7 @@
   A ==> ... ==> C
 *)
 fun conclude th =
-  (case SINGLE (Thm.bicompose_no_flatten false (false, th, Thm.nprems_of th) 1)
+  (case SINGLE (Thm.compose_no_flatten false (th, Thm.nprems_of th) 1)
       (Drule.incr_indexes th Drule.protectD) of
     SOME th' => th'
   | NONE => raise THM ("Failed to conclude goal", 0, [th]));
@@ -145,7 +145,7 @@
     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   in
-    Drule.conj_elim_precise (length props) raw_result
+    hd (Drule.conj_elim_precise [length props] raw_result)
     |> map
       (Drule.implies_intr_list casms
         #> Drule.forall_intr_list cparams
@@ -180,7 +180,7 @@
   init (Thm.adjust_maxidx (Thm.cprem_of st i))
   |> tac
   |> Seq.maps (fn st' =>
-    Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st);
+    Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i st);
 
 in