author | wenzelm |
Fri, 16 Apr 2010 12:51:37 +0200 | |
changeset 36165 | 310a3f2f0e7e |
parent 36164 | 532f4d1cb0fc |
child 36166 | da7b40aa2215 |
--- 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;