1.1 --- a/src/Pure/ML/ml_env.ML	Fri Apr 16 10:52:10 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Fri Apr 16 11:39:08 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val inherit: Context.generic -> Context.generic -> Context.generic
     1.5    val name_space: ML_Name_Space.T
     1.6    val local_context: use_context
     1.7 +  val check_functor: string -> unit
     1.8  end
     1.9  
    1.10  structure ML_Env: ML_ENV =
    1.11 @@ -88,5 +89,11 @@
    1.12    print = writeln,
    1.13    error = error};
    1.14  
    1.15 +val is_functor = is_some o #lookupFunct name_space;
    1.16 +
    1.17 +fun check_functor name =
    1.18 +  if is_functor "Table" (*lookup actually works*) andalso is_functor name then ()
    1.19 +  else error ("Unknown ML functor: " ^ quote name);
    1.20 +
    1.21  end;
    1.22