--- a/src/Pure/Isar/attrib.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Nov 27 21:07:39 2018 +0100
@@ -253,7 +253,8 @@
local
-val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
+val fact_name =
+ Parse.position Args.internal_fact >> (fn (_, pos) => ("<fact>", pos)) || Args.name_position;
fun gen_thm pick = Scan.depend (fn context =>
let
@@ -271,7 +272,7 @@
||
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
>> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
- Scan.ahead (Parse.position fact_name -- Scan.option Parse.thm_sel) :|--
+ Scan.ahead (fact_name -- Scan.option Parse.thm_sel) :|--
(fn ((name, pos), sel) =>
Args.named_fact (get_named (is_some sel) pos) --| Scan.option Parse.thm_sel
>> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))