# HG changeset patch
# User wenzelm
# Date 1271415097 -7200
# Node ID 310a3f2f0e7ee7d9b44a9f3b18fd7bd7d82ae76e
# Parent  532f4d1cb0fca1c48cb20c5626a2e0f147276b20
proper masking of dummy name_space;

diff -r 532f4d1cb0fc -r 310a3f2f0e7e src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Fri Apr 16 11:40:01 2010 +0200
+++ b/src/Pure/ML/ml_env.ML	Fri Apr 16 12:51:37 2010 +0200
@@ -92,7 +92,7 @@
 val is_functor = is_some o #lookupFunct name_space;
 
 fun check_functor name =
-  if is_functor "Table" (*lookup actually works*) andalso is_functor name then ()
+  if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   else error ("Unknown ML functor: " ^ quote name);
 
 end;