src/Pure/Isar/locale.ML

 
 fun activate_elem _ ((ctxt, axs), Fixes fixes) = ((ctxt |> ProofContext.add_fixes fixes, axs), [])
   | activate_elem _ ((ctxt, axs), Assumes asms) =
       let
         val ts = flat (map (map #1 o #2) asms);
-        val n = length ts;
+        val (ps,qs) = splitAt (length ts, axs)
         val (ctxt', _) =
           ctxt |> ProofContext.fix_frees ts
-          |> ProofContext.assume_i (export_axioms (Library.take (n, axs))) asms;
-      in ((ctxt', Library.drop (n, axs)), []) end
+          |> ProofContext.assume_i (export_axioms ps) asms;
+      in ((ctxt', qs), []) end
   | activate_elem _ ((ctxt, axs), Defines defs) =
       let val (ctxt', _) =
         ctxt |> ProofContext.assume_i ProofContext.export_def
           (defs |> map (fn ((name, atts), (t, ps)) =>
             let val (c, t') = ProofContext.cert_def ctxt t

       prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
     val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
 
     val all_propp' = map2 (op ~~)
       (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
-    val n = length raw_concl;
-    val concl = Library.take (n, all_propp');
-    val propp = Library.drop (n, all_propp');
+    val (concl, propp) = splitAt(length raw_concl, all_propp');
     val propps = unflat raw_propps propp;
     val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
 
     val xs = map #1 (params_of raw_elemss);
     val typing = unify_frozen ctxt 0

     val (import_ids, raw_import_elemss) = flatten ([], Expr import);
     val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
 
-    val n = length raw_import_elemss;
+    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
     val ((import_ctxt, axioms'), (import_elemss, _)) =
-      activate_facts prep_facts ((context, axioms), Library.take (n, all_elemss));
+      activate_facts prep_facts ((context, axioms), ps);
     val ((ctxt, _), (elemss, _)) =
-      activate_facts prep_facts ((import_ctxt, axioms'), Library.drop (n, all_elemss));
+      activate_facts prep_facts ((import_ctxt, axioms'), qs);
   in
     ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), concl)
   end;
 
 val gen_context = prep_context_statement intern_expr read_elemss get_facts;

         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;
 
 fun change_elem _ (axms, Assumes asms) =
       apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
-        let val n = length spec
-        in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end))
+        let val (ps,qs) = splitAt(length spec, axs)
+        in (qs, (a, [(ps, [])])) end))
   | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts))
   | change_elem _ e = e;
 
 fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
   (fn (axms, (id as ("", _), es)) =>