1.1 --- a/src/Tools/code/code_target.ML	Tue Jun 24 19:43:21 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Jun 24 19:43:22 2008 +0200
     1.3 @@ -1843,14 +1843,11 @@
     1.4  
     1.5  (* instrumentalization by antiquotation *)
     1.6  
     1.7 -fun ml_code_antiq (ctxt, args) = 
     1.8 +val ml_code_antiq = (Scan.state >> Context.theory_of) -- Scan.repeat1 Args.term >> (fn (thy, ts) =>
     1.9    let
    1.10 -    val thy = Context.theory_of ctxt;
    1.11 -    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
    1.12      val cs = map (CodeUnit.check_const thy) ts;
    1.13      val (cs', program) = CodeThingol.consts_program thy cs;
    1.14 -    val s = sml_code_of thy program cs' ^ " ()";
    1.15 -  in (("codevals", s), (ctxt', args')) end;
    1.16 +  in sml_code_of thy program cs' ^ " ()" end);
    1.17  
    1.18  
    1.19  (* code presentation *)
    1.20 @@ -2294,7 +2291,7 @@
    1.21      | NONE => error ("Bad directive " ^ quote cmd)))
    1.22    handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    1.23  
    1.24 -val _ = ML_Context.value_antiq "code" ml_code_antiq;
    1.25 +val _ = ML_Antiquote.value "code" ml_code_antiq;
    1.26  
    1.27  
    1.28  (* serializer setup, including serializer defaults *)