src/HOL/Tools/specification_package.ML
changeset 17377 afaa031ed4da
parent 17336 c05f72cff368
child 17895 6274b426594b
--- a/src/HOL/Tools/specification_package.ML	Wed Sep 14 10:21:09 2005 +0200
+++ b/src/HOL/Tools/specification_package.ML	Wed Sep 14 10:24:39 2005 +0200
@@ -105,10 +105,10 @@
 fun unvarify t fmap =
     let
         val fmap' = map Library.swap fmap
-        fun unthaw (f as (a,S)) =
-            (case assoc (fmap',a) of
+        fun unthaw (f as (a, S)) =
+            (case AList.lookup (op =) fmap' a of
                  NONE => TVar f
-               | SOME (b, _) => TFree (b,S))
+               | SOME (b, _) => TFree (b, S))
     in
         map_term_types (map_type_tvar unthaw) t
     end