src/Pure/Isar/locale.ML
changeset 16787 b6b6e2faaa41
parent 16736 1e792b32abef
child 16790 be2780f435e1
--- a/src/Pure/Isar/locale.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -705,7 +705,7 @@
 
 fun frozen_tvars ctxt Ts =
   let
-    val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
+    val tvars = rev (fold Term.add_tvarsT Ts []);
     val tfrees = map TFree
       (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
   in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;