# HG changeset patch
# User wenzelm
# Date 1135207758 -3600
# Node ID 5dd6f2f5704f17ec3bc4e5db66897c38175f2cfa
# Parent  c3027c8df1bff56df724f705992dbd5504916a26
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;

diff -r c3027c8df1bf -r 5dd6f2f5704f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Dec 22 00:29:17 2005 +0100
+++ b/src/Pure/goal.ML	Thu Dec 22 00:29:18 2005 +0100
@@ -52,7 +52,7 @@
   A ==> ... ==> C
 *)
 fun conclude th =
-  (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1)
+  (case SINGLE (Thm.bicompose_no_flatten false (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]));
@@ -179,7 +179,8 @@
 fun SELECT tac i st =
   init (Thm.adjust_maxidx (Thm.cprem_of st i))
   |> tac
-  |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
+  |> Seq.maps (fn st' =>
+    Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st);
 
 in