src/Pure/Isar/isar_cmd.ML

 
 (* generic setup *)
 
 fun setup source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
+  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
     "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
+  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
     "Context.map_proof local_setup"
   |> Context.proof_map;
 
 
 (* translation functions *)
 
 fun parse_ast_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
+  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
     "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
   |> Context.theory_map;
 
 fun parse_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parse_translation"
+  |> ML_Context.expression ("parse_translation", Position.thread_data ())
     "(string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.parse_translation parse_translation)"
   |> Context.theory_map;
 
 fun print_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "print_translation"
+  |> ML_Context.expression ("print_translation", Position.thread_data ())
     "(string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.print_translation print_translation)"
   |> Context.theory_map;
 
 fun typed_print_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
+  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
     "(string * (Proof.context -> typ -> term list -> term)) list"
     "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   |> Context.theory_map;
 
 fun print_ast_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
+  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
     "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   |> Context.theory_map;
 
 

 
 (* declarations *)
 
 fun declaration {syntax, pervasive} source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
+  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
       \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   |> Context.proof_map;
 
 
 (* simprocs *)
 
 fun simproc_setup name lhss source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "proc"
+  |> ML_Context.expression ("proc", Position.thread_data ())
     "Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.define_simproc_cmd " ^
       ML_Syntax.atomic (ML_Syntax.make_binding name) ^
       "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
   |> Context.proof_map;