src/Pure/Isar/isar_cmd.ML
changeset 58978 e42da880c61e
parent 58928 23d0ffd48006
child 58979 162a4c2e97bc
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 15:55:31 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 18:16:25 2014 +0100
     1.3 @@ -60,12 +60,14 @@
     1.4  
     1.5  fun global_setup source =
     1.6    ML_Lex.read_source false source
     1.7 -  |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
     1.8 +  |> ML_Context.expression (#range source)
     1.9 +    "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 false source
    1.14 -  |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    1.15 +  |> ML_Context.expression (#range source)
    1.16 +    "val setup: local_theory -> local_theory" "Context.map_proof setup"
    1.17    |> Context.proof_map;
    1.18  
    1.19  
    1.20 @@ -73,35 +75,35 @@
    1.21  
    1.22  fun parse_ast_translation source =
    1.23    ML_Lex.read_source false source
    1.24 -  |> ML_Context.expression (#pos source)
    1.25 +  |> ML_Context.expression (#range source)
    1.26      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.27      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.28    |> Context.theory_map;
    1.29  
    1.30  fun parse_translation source =
    1.31    ML_Lex.read_source false source
    1.32 -  |> ML_Context.expression (#pos source)
    1.33 +  |> ML_Context.expression (#range source)
    1.34      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    1.35      "Context.map_theory (Sign.parse_translation parse_translation)"
    1.36    |> Context.theory_map;
    1.37  
    1.38  fun print_translation source =
    1.39    ML_Lex.read_source false source
    1.40 -  |> ML_Context.expression (#pos source)
    1.41 +  |> ML_Context.expression (#range source)
    1.42      "val print_translation: (string * (Proof.context -> term list -> term)) list"
    1.43      "Context.map_theory (Sign.print_translation print_translation)"
    1.44    |> Context.theory_map;
    1.45  
    1.46  fun typed_print_translation source =
    1.47    ML_Lex.read_source false source
    1.48 -  |> ML_Context.expression (#pos source)
    1.49 +  |> ML_Context.expression (#range source)
    1.50      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    1.51      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    1.52    |> Context.theory_map;
    1.53  
    1.54  fun print_ast_translation source =
    1.55    ML_Lex.read_source false source
    1.56 -  |> ML_Context.expression (#pos source)
    1.57 +  |> ML_Context.expression (#range source)
    1.58      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.59      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.60    |> Context.theory_map;
    1.61 @@ -139,7 +141,7 @@
    1.62          \end;\n");
    1.63    in
    1.64      Context.theory_map
    1.65 -      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
    1.66 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
    1.67    end;
    1.68  
    1.69  
    1.70 @@ -158,7 +160,7 @@
    1.71  
    1.72  fun declaration {syntax, pervasive} source =
    1.73    ML_Lex.read_source false source
    1.74 -  |> ML_Context.expression (#pos source)
    1.75 +  |> ML_Context.expression (#range source)
    1.76      "val declaration: Morphism.declaration"
    1.77      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    1.78        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    1.79 @@ -169,7 +171,7 @@
    1.80  
    1.81  fun simproc_setup name lhss source identifier =
    1.82    ML_Lex.read_source false source
    1.83 -  |> ML_Context.expression (#pos source)
    1.84 +  |> ML_Context.expression (#range source)
    1.85      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.86      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    1.87        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \