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;