src/Pure/Isar/isar_thy.ML

--- a/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -143,7 +143,7 @@
   ("const", (Sign.intern_const, Sign.declared_const, Theory.hide_consts_i))];
 
 fun gen_hide int (kind, xnames) thy =
-  (case assoc_string (kinds, kind) of
+  (case AList.lookup (op =) kinds kind of
     SOME (intern, check, hide) =>
       let
         val names = if int then map (intern thy) xnames else xnames;