src/Pure/Isar/isar_cmd.ML
changeset 56275 600f432ab556
parent 56204 f70e69208a8c
child 56278 2576d3a40ed6
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -145,7 +145,8 @@
     1.4          \  val " ^ name ^
     1.5          " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
     1.6          \end;\n");
     1.7 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
     1.8 +    val flags = {SML = false, verbose = false};
     1.9 +  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
    1.10  
    1.11  
    1.12  (* old-style defs *)
    1.13 @@ -238,7 +239,7 @@
    1.14    let val opt_ctxt =
    1.15      try Toplevel.generic_theory_of state
    1.16      |> Option.map (Context.proof_of #> Diag_State.put state)
    1.17 -  in ML_Context.eval_source_in opt_ctxt verbose source end);
    1.18 +  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
    1.19  
    1.20  val diag_state = Diag_State.get;
    1.21