src/Pure/subgoal.ML
changeset 34075 451b0c8a15cf
parent 32329 1527ff8c2dfb
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/subgoal.ML	Fri Dec 11 15:36:24 2009 +0100
     1.2 +++ b/src/Pure/subgoal.ML	Fri Dec 11 20:43:41 2009 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4        |> fold (Thm.forall_elim o #2) subgoal_inst
     1.5        |> Thm.adjust_maxidx_thm idx
     1.6        |> singleton (Variable.export ctxt2 ctxt0);
     1.7 -  in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
     1.8 +  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
     1.9  
    1.10  
    1.11  (* tacticals *)