--- a/src/Pure/pure_syn.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/pure_syn.ML Tue Mar 18 15:29:58 2014 +0100
@@ -9,8 +9,7 @@
val _ =
Outer_Syntax.command
- (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
- "begin theory context"
+ (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
@@ -18,8 +17,7 @@
val _ =
Outer_Syntax.command
- (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
- "ML text from file"
+ (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
(Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);