Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
authorwenzelm
Fri Dec 11 20:43:41 2009 +0100 (2009-12-11)
changeset 34075451b0c8a15cf
parent 34070 fb0a6419869f
child 34076 e3daf3c07381
Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
src/Pure/subgoal.ML
     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 *)