merged

--- a/NEWS	Fri Dec 11 20:32:58 2009 +0100
+++ b/NEWS	Fri Dec 11 20:44:33 2009 +0100
@@ -13,12 +13,14 @@
 
 * Complete_Lattice.thy: lemmas top_def and bot_def have been replaced
 by the more convenient lemmas Inf_empty and Sup_empty.  Dropped lemmas
-Inf_insert_simp adn Sup_insert_simp, which are subsumed by Inf_insert and
-Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
-Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot respectively.
-INCOMPATIBILITY.
-
-* Finite_Set.thy and List.thy: some lemmas have been generalized from sets to lattices:
+Inf_insert_simp adn Sup_insert_simp, which are subsumed by Inf_insert
+and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ
+and Sup_Univ.  Lemmas inf_top_right and sup_bot_right subsume inf_top
+and sup_bot respectively.  INCOMPATIBILITY.
+
+* Finite_Set.thy and List.thy: some lemmas have been generalized from
+sets to lattices:
+
   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
   inter_Inter_fold_inter        ~> inf_Inf_fold_inf
@@ -33,7 +35,12 @@
 
 *** ML ***
 
-* Curried take and drop;  negative length is interpreted as infinity.  INCOMPATIBILITY.
+* Curried take and drop in library.ML; negative length is interpreted
+as infinity (as in chop).  INCOMPATIBILITY.
+
+* Subgoal.FOCUS (and variants): resulting goal state is normalized as
+usual for resolution.  Rare INCOMPATIBILITY.
+
 
 
 New in Isabelle2009-1 (December 2009)

--- a/src/Pure/subgoal.ML	Fri Dec 11 20:32:58 2009 +0100
+++ b/src/Pure/subgoal.ML	Fri Dec 11 20:44:33 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 *)