1.1 --- a/src/Pure/tactic.ML	Tue Feb 04 08:59:50 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Feb 04 10:33:58 1997 +0100
     1.3 @@ -123,9 +123,9 @@
     1.4  fun defer_tac i state = 
     1.5      let val (state',thaw) = freeze_thaw state
     1.6  	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
     1.7 -	val hyp::hyps' = drop(i-1,hyps)
     1.8 +	val hyp::hyps' = List.drop(hyps, i-1)
     1.9      in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
    1.10 -        |> implies_intr_list (take(i-1,hyps) @ hyps')
    1.11 +        |> implies_intr_list (List.take(hyps, i-1) @ hyps')
    1.12          |> thaw
    1.13          |> Sequence.single
    1.14      end