src/Pure/Isar/parse_spec.ML
changeset 69349 7cef9e386ffe
parent 67740 b6ce18784872
child 72536 589645894305
--- a/src/Pure/Isar/parse_spec.ML	Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Tue Nov 27 21:07:39 2018 +0100
@@ -82,7 +82,7 @@
 
 (* locale and context elements *)
 
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name));
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
 
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
@@ -131,7 +131,7 @@
 
 val locale_expression =
   let
-    val expr2 = Parse.position Parse.name;
+    val expr2 = Parse.name_position;
     val expr1 =
       locale_prefix -- expr2 --
       instance >> (fn ((p, l), i) => (l, (p, i)));