src/Pure/Isar/parse_spec.ML
changeset 46922 3717f3878714
parent 45592 8baa0b7f3f66
child 47067 4ef29b0c568f
--- a/src/Pure/Isar/parse_spec.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -22,7 +22,7 @@
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
-  val class_expr: string list parser
+  val class_expression: string list parser
   val locale_expression: bool -> Expression.expression parser
   val locale_keyword: string parser
   val context_element: Element.context parser
@@ -125,11 +125,11 @@
   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expr = plus1_unless locale_keyword Parse.xname;
+val class_expression = plus1_unless locale_keyword Parse.class;
 
 fun locale_expression mandatory =
   let
-    val expr2 = Parse.xname;
+    val expr2 = Parse.position Parse.xname;
     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;