src/Pure/goal.ML
changeset 18484 5dd6f2f5704f
parent 18252 9e2c15ae0e86
child 18497 7569674d7bb1
     1.1 --- a/src/Pure/goal.ML	Thu Dec 22 00:29:17 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Dec 22 00:29:18 2005 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4    A ==> ... ==> C
     1.5  *)
     1.6  fun conclude th =
     1.7 -  (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1)
     1.8 +  (case SINGLE (Thm.bicompose_no_flatten false (false, th, Thm.nprems_of th) 1)
     1.9        (Drule.incr_indexes th Drule.protectD) of
    1.10      SOME th' => th'
    1.11    | NONE => raise THM ("Failed to conclude goal", 0, [th]));
    1.12 @@ -179,7 +179,8 @@
    1.13  fun SELECT tac i st =
    1.14    init (Thm.adjust_maxidx (Thm.cprem_of st i))
    1.15    |> tac
    1.16 -  |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
    1.17 +  |> Seq.maps (fn st' =>
    1.18 +    Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st);
    1.19  
    1.20  in
    1.21