src/Pure/ML/ml_env.ML

--- a/src/Pure/ML/ml_env.ML	Fri Apr 16 10:52:10 2010 +0200
+++ b/src/Pure/ML/ml_env.ML	Fri Apr 16 11:39:08 2010 +0200
@@ -9,6 +9,7 @@
   val inherit: Context.generic -> Context.generic -> Context.generic
   val name_space: ML_Name_Space.T
   val local_context: use_context
+  val check_functor: string -> unit
 end
 
 structure ML_Env: ML_ENV =
@@ -88,5 +89,11 @@
   print = writeln,
   error = error};
 
+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 ()
+  else error ("Unknown ML functor: " ^ quote name);
+
 end;