src/Pure/tactic.ML
changeset 2580 e3f680709487
parent 2228 f381c1a98209
child 2672 85d7e800d754
--- a/src/Pure/tactic.ML	Tue Feb 04 08:59:50 1997 +0100
+++ b/src/Pure/tactic.ML	Tue Feb 04 10:33:58 1997 +0100
@@ -123,9 +123,9 @@
 fun defer_tac i state = 
     let val (state',thaw) = freeze_thaw state
 	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
-	val hyp::hyps' = drop(i-1,hyps)
+	val hyp::hyps' = List.drop(hyps, i-1)
     in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
-        |> implies_intr_list (take(i-1,hyps) @ hyps')
+        |> implies_intr_list (List.take(hyps, i-1) @ hyps')
         |> thaw
         |> Sequence.single
     end