# HG changeset patch
# User wenzelm
# Date 1260560621 -3600
# Node ID 451b0c8a15cfef76a23ecf320d8fab584fe0cf6b
# Parent  fb0a6419869f9ed0f293beea821dd0ce4f6150c7
Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;

diff -r fb0a6419869f -r 451b0c8a15cf src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Fri Dec 11 15:36:24 2009 +0100
+++ b/src/Pure/subgoal.ML	Fri Dec 11 20:43:41 2009 +0100
@@ -125,7 +125,7 @@
       |> fold (Thm.forall_elim o #2) subgoal_inst
       |> Thm.adjust_maxidx_thm idx
       |> singleton (Variable.export ctxt2 ctxt0);
-  in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
+  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
 
 
 (* tacticals *)