src/Pure/Isar/isar_cmd.ML
changeset 56278 2576d3a40ed6
parent 56275 600f432ab556
child 56304 40274e4f5ebf
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 15:15:33 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 16:11:00 2014 +0100
     1.3 @@ -67,12 +67,12 @@
     1.4  (* generic setup *)
     1.5  
     1.6  fun global_setup source =
     1.7 -  ML_Lex.read_source source
     1.8 +  ML_Lex.read_source false source
     1.9    |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
    1.10    |> Context.theory_map;
    1.11  
    1.12  fun local_setup source =
    1.13 -  ML_Lex.read_source source
    1.14 +  ML_Lex.read_source false source
    1.15    |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    1.16    |> Context.proof_map;
    1.17  
    1.18 @@ -80,35 +80,35 @@
    1.19  (* translation functions *)
    1.20  
    1.21  fun parse_ast_translation source =
    1.22 -  ML_Lex.read_source source
    1.23 +  ML_Lex.read_source false source
    1.24    |> ML_Context.expression (#pos source)
    1.25      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.26      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.27    |> Context.theory_map;
    1.28  
    1.29  fun parse_translation source =
    1.30 -  ML_Lex.read_source source
    1.31 +  ML_Lex.read_source false source
    1.32    |> ML_Context.expression (#pos source)
    1.33      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    1.34      "Context.map_theory (Sign.parse_translation parse_translation)"
    1.35    |> Context.theory_map;
    1.36  
    1.37  fun print_translation source =
    1.38 -  ML_Lex.read_source source
    1.39 +  ML_Lex.read_source false source
    1.40    |> ML_Context.expression (#pos source)
    1.41      "val print_translation: (string * (Proof.context -> term list -> term)) list"
    1.42      "Context.map_theory (Sign.print_translation print_translation)"
    1.43    |> Context.theory_map;
    1.44  
    1.45  fun typed_print_translation source =
    1.46 -  ML_Lex.read_source source
    1.47 +  ML_Lex.read_source false source
    1.48    |> ML_Context.expression (#pos source)
    1.49      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    1.50      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    1.51    |> Context.theory_map;
    1.52  
    1.53  fun print_ast_translation source =
    1.54 -  ML_Lex.read_source source
    1.55 +  ML_Lex.read_source false source
    1.56    |> ML_Context.expression (#pos source)
    1.57      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.58      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.59 @@ -135,7 +135,7 @@
    1.60  
    1.61  fun oracle (name, pos) source =
    1.62    let
    1.63 -    val body = ML_Lex.read_source source;
    1.64 +    val body = ML_Lex.read_source false source;
    1.65      val ants =
    1.66        ML_Lex.read Position.none
    1.67         ("local\n\
    1.68 @@ -162,7 +162,7 @@
    1.69  (* declarations *)
    1.70  
    1.71  fun declaration {syntax, pervasive} source =
    1.72 -  ML_Lex.read_source source
    1.73 +  ML_Lex.read_source false source
    1.74    |> ML_Context.expression (#pos source)
    1.75      "val declaration: Morphism.declaration"
    1.76      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    1.77 @@ -173,7 +173,7 @@
    1.78  (* simprocs *)
    1.79  
    1.80  fun simproc_setup name lhss source identifier =
    1.81 -  ML_Lex.read_source source
    1.82 +  ML_Lex.read_source false source
    1.83    |> ML_Context.expression (#pos source)
    1.84      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.85      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \