src/Pure/Isar/isar_cmd.ML
changeset 69268 c546e37f6cb9
parent 69221 1a52baa70aed
child 70064 f8293bf510a0
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Nov 08 13:42:36 2018 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Nov 08 14:48:20 2018 +0100
     1.3 @@ -113,23 +113,15 @@
     1.4  (* oracles *)
     1.5  
     1.6  fun oracle (name, range) source =
     1.7 -  let
     1.8 -    val body_range = Input.range_of source;
     1.9 -    val body = ML_Lex.read_source source;
    1.10 -
    1.11 -    val ants =
    1.12 -      ML_Lex.read
    1.13 -       ("local\n\
    1.14 -        \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
    1.15 -        \  val") @ ML_Lex.read_set_range body_range "oracle" @ ML_Lex.read "=" @ body @
    1.16 -        ML_Lex.read (";\nin\n\
    1.17 -        \  val") @ ML_Lex.read_set_range range name @ ML_Lex.read "=\
    1.18 -        \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    1.19 -        \end;\n";
    1.20 -  in
    1.21 -    Context.theory_map
    1.22 -      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 body_range) ants))
    1.23 -  end;
    1.24 +  ML_Context.expression (Input.pos_of source)
    1.25 +    (ML_Lex.read "val " @
    1.26 +     ML_Lex.read_set_range range name @
    1.27 +     ML_Lex.read
    1.28 +      (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^
    1.29 +        ML_Syntax.make_binding (name, #1 range) ^ ", ") @
    1.30 +     ML_Lex.read_source source @
    1.31 +     ML_Lex.read "))))")
    1.32 +  |> Context.theory_map;
    1.33  
    1.34  
    1.35  (* declarations *)