Gradual switching to Basis Library functions nth, drop, etc.

--- a/src/Pure/goals.ML	Tue Feb 04 08:59:50 1997 +0100
+++ b/src/Pure/goals.ML	Tue Feb 04 10:33:58 1997 +0100
@@ -42,6 +42,7 @@
   val goalw_cterm	: thm list -> cterm -> thm list
   val pop_proof		: unit -> thm list
   val pr		: unit -> unit
+  val prlev		: int -> unit
   val prlim		: int -> unit
   val pr_latex		: unit -> unit
   val printgoal_latex	: int -> unit
@@ -52,7 +53,6 @@
   val pprint_typ	: typ -> pprint_args -> unit
   val print_exn		: exn -> 'a
   val print_sign_exn	: Sign.sg -> exn -> 'a
-  val prlev		: int -> unit
   val proof_timing	: bool ref
   val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
   val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
@@ -260,10 +260,8 @@
 fun uresult () = !curr_mkresult (false, topthm());
 
 (*Get subgoal i from goal stack*)
-fun getgoal i = 
-      (case  drop (i-1, prems_of (topthm()))  of
-	    [] => error"getgoal: Goal number out of range"
-	  | Q::_ => Q);
+fun getgoal i = List.nth (prems_of (topthm()), i-1)
+                handle Subscript => error"getgoal: Goal number out of range";
 
 (*Return subgoal i's hypotheses as meta-level assumptions.
   For debugging uses of METAHYPS*)
@@ -281,9 +279,9 @@
 fun chop_level n (pair,pairs) = 
   let val level = length pairs
   in  if n<0 andalso ~n <= level
-      then  drop (~n, pair::pairs) 
+      then  List.drop (pair::pairs, ~n) 
       else if 0<=n andalso n<= level
-      then  drop (level - n, pair::pairs) 
+      then  List.drop (pair::pairs, level - n) 
       else  error ("Level number must lie between 0 and " ^ 
 		   string_of_int level)
   end;

--- 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

--- a/src/Pure/tctical.ML	Tue Feb 04 08:59:50 1997 +0100
+++ b/src/Pure/tctical.ML	Tue Feb 04 10:33:58 1997 +0100
@@ -304,10 +304,8 @@
 
 
 (*Make a tactic for subgoal i, if there is one.  *)
-fun SUBGOAL goalfun i st = 
-  case drop(i-1, prems_of st) of
-      [] => Sequence.null
-    | prem::_ => goalfun (prem,i) st;
+fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
+                             handle Subscript => Sequence.null;
 
 
 (*** SELECT_GOAL ***)
@@ -346,9 +344,8 @@
 
 (*Does the work of SELECT_GOAL. *)
 fun select tac st0 i =
-  let val cprem::_ = drop(i-1, cprems_of st0)
-      val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
-                                eq_trivial (adjust_maxidx cprem)
+  let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
+	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
       fun next st = bicompose false (false, restore st, nprems_of st) i st0
   in  Sequence.flats (Sequence.maps next (tac eq_cprem))
   end;
@@ -365,7 +362,7 @@
         handle _ => error"SELECT_GOAL -- impossible error???";
 
 fun SELECT_GOAL tac i st = 
-  case (i, drop(i-1, prems_of st)) of
+  case (i, List.drop(prems_of st, i-1)) of
       (_,[]) => Sequence.null
     | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
     | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i

--- a/src/Pure/term.ML	Tue Feb 04 08:59:50 1997 +0100
+++ b/src/Pure/term.ML	Tue Feb 04 10:33:58 1997 +0100
@@ -294,10 +294,9 @@
 fun subst_bounds (args: term list, t) : term = 
   let val n = length args;
       fun subst (t as Bound i, lev) =
- 	    if i<lev then  t    (*var is locally bound*)
-	    else  (case (drop (i-lev,args)) of
-		  []     => Bound(i-n)  (*loose: change it*)
-	        | arg::_ => incr_boundvars lev arg)
+ 	   (if i<lev then  t    (*var is locally bound*)
+	    else  incr_boundvars lev (List.nth(args, i-lev))
+		    handle Subscript => Bound(i-n)  (*loose: change it*))
 	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
 	| subst (t,lev) = t