1.1 --- a/doc-src/antiquote_setup.ML	Fri Apr 16 10:52:10 2010 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Fri Apr 16 11:39:08 2010 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
     1.6  
     1.7 -fun ml_functor _ = "";  (*no check!*)
     1.8 +fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
     1.9  
    1.10  fun index_ml name kind ml = ThyOutput.antiquotation name
    1.11    (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))

     2.1 --- a/src/Pure/ML/ml_env.ML	Fri Apr 16 10:52:10 2010 +0200
     2.2 +++ b/src/Pure/ML/ml_env.ML	Fri Apr 16 11:39:08 2010 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4    val inherit: Context.generic -> Context.generic -> Context.generic
     2.5    val name_space: ML_Name_Space.T
     2.6    val local_context: use_context
     2.7 +  val check_functor: string -> unit
     2.8  end
     2.9  
    2.10  structure ML_Env: ML_ENV =
    2.11 @@ -88,5 +89,11 @@
    2.12    print = writeln,
    2.13    error = error};
    2.14  
    2.15 +val is_functor = is_some o #lookupFunct name_space;
    2.16 +
    2.17 +fun check_functor name =
    2.18 +  if is_functor "Table" (*lookup actually works*) andalso is_functor name then ()
    2.19 +  else error ("Unknown ML functor: " ^ quote name);
    2.20 +
    2.21  end;
    2.22  

     3.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 16 10:52:10 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Apr 16 11:39:08 2010 +0200
     3.3 @@ -599,7 +599,7 @@
     3.4  val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
     3.5  val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
     3.6  val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
     3.7 -val _ = ml_text "ML_functor" (K "");  (*no check!*)
     3.8 +val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
     3.9  val _ = ml_text "ML_text" (K "");
    3.10  
    3.11  end;