1.1 --- a/src/Pure/ML/ml_context.ML	Tue Dec 18 19:54:33 2007 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Tue Dec 18 19:54:34 2007 +0100
     1.3 @@ -71,9 +71,9 @@
     1.4      (y, SOME context') => (y, context')
     1.5    | (_, NONE) => error "Lost context in ML");
     1.6  
     1.7 -fun save f x = CRITICAL (fn () => setmp (get_context ()) f x);
     1.8 +fun save f x = NAMED_CRITICAL "ML" (fn () => setmp (get_context ()) f x);
     1.9  
    1.10 -fun change_theory f = CRITICAL (fn () =>
    1.11 +fun change_theory f = NAMED_CRITICAL "ML" (fn () =>
    1.12    set_context (SOME (Context.map_theory f (the_generic_context ()))));
    1.13  
    1.14  
    1.15 @@ -141,7 +141,7 @@
    1.16  val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
    1.17  val isabelle_struct0 = isabelle_struct "";
    1.18  
    1.19 -fun eval_antiquotes txt = CRITICAL (fn () =>
    1.20 +fun eval_antiquotes txt =
    1.21    let
    1.22      val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
    1.23  
    1.24 @@ -160,9 +160,9 @@
    1.25                in ((binding, value), names') end);
    1.26  
    1.27      val (decls, body) =
    1.28 -      fold_map expand ants ML_Syntax.reserved
    1.29 +      NAMED_CRITICAL "ML" (fn () => fold_map expand ants ML_Syntax.reserved)
    1.30        |> #1 |> split_list |> pairself implode;
    1.31 -  in (isabelle_struct decls, body) end);
    1.32 +  in (isabelle_struct decls, body) end;
    1.33  
    1.34  in
    1.35  
    1.36 @@ -198,7 +198,7 @@
    1.37  
    1.38  fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path);
    1.39  
    1.40 -fun evaluate pr verbose (ref_name, r) txt = CRITICAL (fn () =>
    1.41 +fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
    1.42    let
    1.43      val _ = r := NONE;
    1.44      val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");