src/Pure/Pure.thy
changeset 62873 2f9c8a18f832
parent 62867 cce0570d1bfa
child 62898 fdc290b68ecd
     1.1 --- a/src/Pure/Pure.thy	Tue Apr 05 18:18:36 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Apr 05 18:20:25 2016 +0200
     1.3 @@ -133,8 +133,8 @@
     1.4      (Parse.ML_source >> (fn source =>
     1.5        let
     1.6          val flags: ML_Compiler.flags =
     1.7 -          {SML = true, exchange = true, redirect = false, verbose = true,
     1.8 -            debug = NONE, writeln = writeln, warning = warning};
     1.9 +          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
    1.10 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.11        in
    1.12          Toplevel.theory
    1.13            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    1.14 @@ -145,8 +145,8 @@
    1.15      (Parse.ML_source >> (fn source =>
    1.16        let
    1.17          val flags: ML_Compiler.flags =
    1.18 -          {SML = false, exchange = true, redirect = false, verbose = true,
    1.19 -            debug = NONE, writeln = writeln, warning = warning};
    1.20 +          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
    1.21 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.22        in
    1.23          Toplevel.generic_theory
    1.24            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>