src/Pure/Isar/isar_cmd.ML
changeset 56304 40274e4f5ebf
parent 56278 2576d3a40ed6
child 56334 6b3739fee456
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:12:40 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 17:56:13 2014 +0100
     1.3 @@ -145,8 +145,10 @@
     1.4          \  val " ^ name ^
     1.5          " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
     1.6          \end;\n");
     1.7 -    val flags = {SML = false, verbose = false};
     1.8 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
     1.9 +  in
    1.10 +    Context.theory_map
    1.11 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
    1.12 +  end;
    1.13  
    1.14  
    1.15  (* old-style defs *)
    1.16 @@ -236,10 +238,12 @@
    1.17  );
    1.18  
    1.19  fun ml_diag verbose source = Toplevel.keep (fn state =>
    1.20 -  let val opt_ctxt =
    1.21 -    try Toplevel.generic_theory_of state
    1.22 -    |> Option.map (Context.proof_of #> Diag_State.put state)
    1.23 -  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
    1.24 +  let
    1.25 +    val opt_ctxt =
    1.26 +      try Toplevel.generic_theory_of state
    1.27 +      |> Option.map (Context.proof_of #> Diag_State.put state);
    1.28 +    val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
    1.29 +  in ML_Context.eval_source_in opt_ctxt flags source end);
    1.30  
    1.31  val diag_state = Diag_State.get;
    1.32