src/Pure/Isar/isar_cmd.ML
changeset 59067 dd8ec9138112
parent 59064 a8bcb5a446c8
child 59206 36808125e00f
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 13:15:04 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 14:02:48 2014 +0100
     1.3 @@ -131,15 +131,13 @@
     1.4      val body_range = Input.range_of source;
     1.5      val body = ML_Lex.read_source false source;
     1.6  
     1.7 -    val hidden = ML_Lex.read Position.none;
     1.8 -    val visible = ML_Lex.read_set_range;
     1.9      val ants =
    1.10 -      hidden
    1.11 +      ML_Lex.read
    1.12         ("local\n\
    1.13          \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
    1.14 -        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
    1.15 -        \in\n\
    1.16 -        \  val") @ visible range name @ hidden "=\
    1.17 +        \  val") @ ML_Lex.read_set_range body_range "oracle" @ ML_Lex.read "=" @ body @
    1.18 +        ML_Lex.read (";\nin\n\
    1.19 +        \  val") @ ML_Lex.read_set_range range name @ ML_Lex.read "=\
    1.20          \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    1.21          \end;\n";
    1.22    in