src/Pure/goal.ML
changeset 18145 6757627acf59
parent 18139 b15981aedb7b
child 18180 db712213504d
     1.1 --- a/src/Pure/goal.ML	Thu Nov 10 17:33:14 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Nov 10 20:57:11 2005 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  (* composition of normal results *)
     1.5  
     1.6  fun compose_hhf tha i thb =
     1.7 -  Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
     1.8 +  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
     1.9  
    1.10  fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
    1.11  
    1.12 @@ -161,7 +161,7 @@
    1.13    composing the resulting thm with the original state.*)
    1.14  
    1.15  fun SELECT tac i st =
    1.16 -  init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1)))
    1.17 +  init (Thm.adjust_maxidx (Thm.cprem_of st i))
    1.18    |> tac
    1.19    |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
    1.20