proper masking of dummy name_space;

--- 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;