src/Pure/goal.ML
changeset 18497 7569674d7bb1
parent 18484 5dd6f2f5704f
child 18678 dd0c569fa43d
     1.1 --- a/src/Pure/goal.ML	Fri Dec 23 15:16:44 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Fri Dec 23 15:16:46 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_no_flatten false (false, th, Thm.nprems_of th) 1)
     1.8 +  (case SINGLE (Thm.compose_no_flatten 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 @@ -145,7 +145,7 @@
    1.13      val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
    1.14        err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
    1.15    in
    1.16 -    Drule.conj_elim_precise (length props) raw_result
    1.17 +    hd (Drule.conj_elim_precise [length props] raw_result)
    1.18      |> map
    1.19        (Drule.implies_intr_list casms
    1.20          #> Drule.forall_intr_list cparams
    1.21 @@ -180,7 +180,7 @@
    1.22    init (Thm.adjust_maxidx (Thm.cprem_of st i))
    1.23    |> tac
    1.24    |> Seq.maps (fn st' =>
    1.25 -    Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st);
    1.26 +    Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i st);
    1.27  
    1.28  in
    1.29