src/Pure/Isar/isar_cmd.ML
changeset 69188 d8849cfad60f
parent 68823 5e7b1ae10eb8
child 69221 1a52baa70aed
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 17:08:04 2018 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 21:29:08 2018 +0200
     1.3 @@ -52,13 +52,13 @@
     1.4  
     1.5  fun setup source =
     1.6    ML_Lex.read_source source
     1.7 -  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
     1.8 +  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
     1.9      "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_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
    1.15 +  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
    1.16      "Context.map_proof local_setup"
    1.17    |> Context.proof_map;
    1.18  
    1.19 @@ -67,35 +67,35 @@
    1.20  
    1.21  fun parse_ast_translation source =
    1.22    ML_Lex.read_source source
    1.23 -  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
    1.24 +  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
    1.25      "(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_Context.expression (Input.range_of source) "parse_translation"
    1.32 +  |> ML_Context.expression ("parse_translation", Position.thread_data ())
    1.33      "(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_Context.expression (Input.range_of source) "print_translation"
    1.40 +  |> ML_Context.expression ("print_translation", Position.thread_data ())
    1.41      "(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_Context.expression (Input.range_of source) "typed_print_translation"
    1.48 +  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
    1.49      "(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_Context.expression (Input.range_of source) "print_ast_translation"
    1.56 +  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
    1.57      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.58      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.59    |> Context.theory_map;
    1.60 @@ -143,7 +143,7 @@
    1.61  
    1.62  fun declaration {syntax, pervasive} source =
    1.63    ML_Lex.read_source source
    1.64 -  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
    1.65 +  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
    1.66      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    1.67        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    1.68    |> Context.proof_map;
    1.69 @@ -153,7 +153,7 @@
    1.70  
    1.71  fun simproc_setup name lhss source =
    1.72    ML_Lex.read_source source
    1.73 -  |> ML_Context.expression (Input.range_of source) "proc"
    1.74 +  |> ML_Context.expression ("proc", Position.thread_data ())
    1.75      "Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.76      ("Context.map_proof (Simplifier.define_simproc_cmd " ^
    1.77        ML_Syntax.atomic (ML_Syntax.make_binding name) ^