src/Pure/Isar/locale.ML

       val t = termify ts;
       val subs = subsumers sign t regs;
     in (case subs of
         [] => NONE
       | ((t', (attn, thms)) :: _) => let
-            val (tinst, inst) = Pattern.match sign (t', t);
+            val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty);
             (* thms contain Frees, not Vars *)
             val tinst' = tinst |> Vartab.dest
                  |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T))
                  |> Symtab.make;
             val inst' = inst |> Vartab.dest

 
     val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
     val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
     val thy = ProofContext.theory_of ctxt;
 
-    fun unify (env, (SOME T, SOME U)) = (Sign.typ_unify thy (U, T) env
-          handle Type.TUNIFY =>
-            raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
-      | unify (env, _) = env;
-    val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');
+    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
+          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
+      | unify _ env = env;
+    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
   in map (Option.map (Envir.norm_type unifier')) Vs end;
 
 fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));

   in (Term.dest_Free f, eq') end;
 
 fun abstract_thm thy eq =
   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
 
-fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
+fun bind_def ctxt (name, ps) eq (xs, env, ths) =
   let
     val ((y, T), b) = abstract_term eq;
     val b' = norm_term env b;
     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];

 
 
 (* CB: for finish_elems (Int and Ext),
    extracts specification, only of assumed elements *)
 
-fun eval_text _ _ _ (text, Fixes _) = text
-  | eval_text _ _ _ (text, Constrains _) = text
-  | eval_text _ (_, Assumed _) is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
+fun eval_text _ _ _ (Fixes _) text = text
+  | eval_text _ _ _ (Constrains _) text = text
+  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
+        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
       let
         val ts = List.concat (map (map #1 o #2) asms);
         val ts' = map (norm_term env) ts;
         val spec' =
           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
           else ((exts, exts'), (ints @ ts, ints' @ ts'));
       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
-  | eval_text _ (_, Derived _) _ (text, Assumes _) = text
-  | eval_text ctxt (id, Assumed _) _ ((spec, binds), Defines defs) =
-      (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
-  | eval_text _ (_, Derived _) _ (text, Defines _) = text
-  | eval_text _ _ _ (text, Notes _) = text;
+  | eval_text _ (_, Derived _) _ (Assumes _) text = text
+  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
+      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
+  | eval_text _ (_, Derived _) _ (Defines _) text = text
+  | eval_text _ _ _ (Notes _) text = text;
 
 
 (* for finish_elems (Int),
    remove redundant elements of derived identifiers,
    turn assumptions and definitions into facts,

 
 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
       let
         val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
-        val text' = Library.foldl (eval_text ctxt id' false) (text, es);
+        val text' = fold (eval_text ctxt id' false) es text;
         val es' = List.mapPartial
               (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
       in ((text', wits'), (id', map Int es')) end
   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
       let
         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
-        val text' = eval_text ctxt id true (text, e');
+        val text' = eval_text ctxt id true e' text;
       in ((text', wits), (id, [Ext e'])) end
 
 in
 
 (* CB: only called by prep_elemss *)

 
     val regs = get_global_registrations thy target;
 
     (* add args to thy for all registrations *)
 
-    fun activate (thy, (vts, ((prfx, atts2), _))) =
+    fun activate (vts, ((prfx, atts2), _)) thy =
       let
         val (insts, prems) = collect_global_witnesses thy parms ids vts;
         val inst_atts =
           Args.map_values I (Element.instT_type (#1 insts))
             (Element.inst_term insts) (Element.inst_thm thy insts);

             ((NameSpace.qualified prfx n,
               map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)),
              [(map (Drule.standard o satisfy_protected prems o
             Element.inst_thm thy insts) ths, [])]));
       in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
-  in Library.foldl activate (thy, regs) end;
+  in fold activate regs thy end;
 
 
 fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
   | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;