src/Pure/Isar/spec_parse.ML
changeset 29360 a5be60c3674e
parent 29312 f369fb19146e
child 29581 b3b33e0298eb
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Mon Jan 05 15:37:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Mon Jan 05 15:55:04 2009 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4    val locale_fixes: (Binding.T * string option * mixfix) list parser
     1.5    val locale_insts: (string option list * (Attrib.binding * string) list) parser
     1.6    val class_expr: string list parser
     1.7 -  val locale_expr: Locale.expr parser
     1.8 +  val locale_expr: Old_Locale.expr parser
     1.9    val locale_expression: Expression.expression parser
    1.10    val locale_keyword: string parser
    1.11    val context_element: Element.context parser
    1.12 @@ -117,9 +117,9 @@
    1.13  
    1.14  val locale_expr =
    1.15    let
    1.16 -    fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
    1.17 -    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
    1.18 -    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.19 +    fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
    1.20 +    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
    1.21 +    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
    1.22    in expr0 end;
    1.23  
    1.24  val locale_expression =