src/Pure/Isar/spec_parse.ML
changeset 29581 b3b33e0298eb
parent 29360 a5be60c3674e
child 29601 93553f7c722f
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -15,24 +15,23 @@
     1.4    val opt_thm_name: string -> Attrib.binding parser
     1.5    val spec: (Attrib.binding * string list) parser
     1.6    val named_spec: (Attrib.binding * string list) parser
     1.7 -  val spec_name: ((Binding.T * string) * Attrib.src list) parser
     1.8 -  val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
     1.9 +  val spec_name: ((binding * string) * Attrib.src list) parser
    1.10 +  val spec_opt_name: ((binding * string) * Attrib.src list) parser
    1.11    val xthm: (Facts.ref * Attrib.src list) parser
    1.12    val xthms1: (Facts.ref * Attrib.src list) list parser
    1.13    val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    1.14    val locale_mixfix: mixfix parser
    1.15 -  val locale_fixes: (Binding.T * string option * mixfix) list parser
    1.16 +  val locale_fixes: (binding * string option * mixfix) list parser
    1.17    val locale_insts: (string option list * (Attrib.binding * string) list) parser
    1.18    val class_expr: string list parser
    1.19 -  val locale_expr: Old_Locale.expr parser
    1.20 -  val locale_expression: Expression.expression parser
    1.21 +    val locale_expression: Expression.expression parser
    1.22    val locale_keyword: string parser
    1.23    val context_element: Element.context parser
    1.24    val statement: (Attrib.binding * (string * string list) list) list parser
    1.25    val general_statement: (Element.context list * Element.statement) parser
    1.26    val statement_keyword: string parser
    1.27    val specification:
    1.28 -    (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
    1.29 +    (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
    1.30  end;
    1.31  
    1.32  structure SpecParse: SPEC_PARSE =
    1.33 @@ -115,13 +114,6 @@
    1.34  
    1.35  val class_expr = plus1_unless locale_keyword P.xname;
    1.36  
    1.37 -val locale_expr =
    1.38 -  let
    1.39 -    fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
    1.40 -    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
    1.41 -    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
    1.42 -  in expr0 end;
    1.43 -
    1.44  val locale_expression =
    1.45    let
    1.46      fun expr2 x = P.xname x;