# HG changeset patch
# User wenzelm
# Date 1273959135 -7200
# Node ID 338c3f8229e467539891666863b7a46ac81e80eb
# Parent  985c197f2fe9752f4c644c3d928c85164efe4dd5
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

diff -r 985c197f2fe9 -r 338c3f8229e4 NEWS
--- a/NEWS	Sat May 15 23:23:45 2010 +0200
+++ b/NEWS	Sat May 15 23:32:15 2010 +0200
@@ -507,6 +507,7 @@
 
   OuterKeyword  ~>  Keyword
   OuterParse    ~>  Parse
+  SpecParse     ~>  Parse_Spec
 
 
 *** System ***
diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat May 15 23:23:45 2010 +0200
+++ b/src/Pure/IsaMakefile	Sat May 15 23:32:15 2010 +0200
@@ -69,10 +69,10 @@
   Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
   Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
   Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
-  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
-  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
-  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
-  Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML		\
+  Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
+  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
+  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
+  Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
   Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
   ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
   ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat May 15 23:23:45 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 15 23:32:15 2010 +0200
@@ -183,7 +183,7 @@
 
 val _ =
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
-    (Scan.repeat1 SpecParse.spec >>
+    (Scan.repeat1 Parse_Spec.spec >>
       (Toplevel.theory o
         (IsarCmd.add_axioms o
           tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
@@ -196,7 +196,7 @@
 val _ =
   OuterSyntax.command "defs" "define constants" Keyword.thy_decl
     (opt_unchecked_overloaded --
-      Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
+      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
@@ -208,7 +208,7 @@
     --| Scan.option Parse.where_ >> Parse.triple1 ||
   Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
 
-val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop);
+val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop);
 
 val structs =
   Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
@@ -223,11 +223,11 @@
 
 val _ =
   OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
-    (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
+    (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
 
 val _ =
   OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
-    (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop)
+    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
       >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
@@ -245,13 +245,13 @@
 val _ =
   OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
   OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
@@ -260,14 +260,14 @@
 val _ =
   OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
     (Scan.optional Parse.fixes [] --
-      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) []
+      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
       >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
 
 
 (* theorems *)
 
 fun theorems kind =
-  SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
+  Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
 
 val _ =
   OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
@@ -277,7 +277,7 @@
 
 val _ =
   OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
-    (Parse.and_list1 SpecParse.xthms1
+    (Parse.and_list1 Parse_Spec.xthms1
       >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
 
 
@@ -416,9 +416,9 @@
 (* locales *)
 
 val locale_val =
-  SpecParse.locale_expression false --
-    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair ([], []);
+  Parse_Spec.locale_expression false --
+    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
 val _ =
   OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
@@ -432,15 +432,15 @@
   OuterSyntax.command "sublocale"
     "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
     (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
-      Parse.!!! (SpecParse.locale_expression false)
+      Parse.!!! (Parse_Spec.locale_expression false)
       >> (fn (loc, expr) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
 
 val _ =
   OuterSyntax.command "interpretation"
     "prove interpretation of locale expression in theory" Keyword.thy_goal
-    (Parse.!!! (SpecParse.locale_expression true) --
-      Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) []
+    (Parse.!!! (Parse_Spec.locale_expression true) --
+      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
 
@@ -448,16 +448,16 @@
   OuterSyntax.command "interpret"
     "prove interpretation of locale expression in proof context"
     (Keyword.tag_proof Keyword.prf_goal)
-    (Parse.!!! (SpecParse.locale_expression true)
+    (Parse.!!! (Parse_Spec.locale_expression true)
       >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
 
 
 (* classes *)
 
 val class_val =
-  SpecParse.class_expr --
-    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair [];
+  Parse_Spec.class_expr --
+    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+  Scan.repeat1 Parse_Spec.context_element >> pair [];
 
 val _ =
   OuterSyntax.command "class" "define type class" Keyword.thy_decl
@@ -514,9 +514,9 @@
     (if schematic then "schematic_" ^ kind else kind)
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
     (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
-    (Scan.optional (SpecParse.opt_thm_name ":" --|
-      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
-      SpecParse.general_statement >> (fn (a, (elems, concl)) =>
+    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
+      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
+      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
           kind NONE (K I) a elems concl)));
 
@@ -537,27 +537,27 @@
 val _ =
   OuterSyntax.command "have" "state local goal"
     (Keyword.tag_proof Keyword.prf_goal)
-    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
+    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
 
 val _ =
   OuterSyntax.command "hence" "abbreviates \"then have\""
     (Keyword.tag_proof Keyword.prf_goal)
-    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
+    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
 
 val _ =
   OuterSyntax.command "show" "state local goal, solving current obligation"
     (Keyword.tag_proof Keyword.prf_asm_goal)
-    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
+    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
 
 val _ =
   OuterSyntax.command "thus" "abbreviates \"then show\""
     (Keyword.tag_proof Keyword.prf_asm_goal)
-    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
+    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
 
 
 (* facts *)
 
-val facts = Parse.and_list1 SpecParse.xthms1;
+val facts = Parse.and_list1 Parse_Spec.xthms1;
 
 val _ =
   OuterSyntax.command "then" "forward chaining"
@@ -577,7 +577,7 @@
 val _ =
   OuterSyntax.command "note" "define facts"
     (Keyword.tag_proof Keyword.prf_decl)
-    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
+    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "using" "augment goal facts"
@@ -600,18 +600,18 @@
 val _ =
   OuterSyntax.command "assume" "assume propositions"
     (Keyword.tag_proof Keyword.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
 
 val _ =
   OuterSyntax.command "presume" "assume propositions, to be established later"
     (Keyword.tag_proof Keyword.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
 
 val _ =
   OuterSyntax.command "def" "local definition"
     (Keyword.tag_proof Keyword.prf_asm)
     (Parse.and_list1
-      (SpecParse.opt_thm_name ":" --
+      (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
           ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
@@ -619,7 +619,7 @@
 val _ =
   OuterSyntax.command "obtain" "generalized existence"
     (Keyword.tag_proof Keyword.prf_asm_goal)
-    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement
+    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
@@ -636,13 +636,13 @@
 val _ =
   OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
     (Keyword.tag_proof Keyword.prf_decl)
-    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =
   (Parse.$$$ "(" |--
     Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
-    Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1;
+    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
 
 val _ =
   OuterSyntax.command "case" "invoke local context"
@@ -739,7 +739,7 @@
 (* calculational proof commands *)
 
 val calc_args =
-  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")")));
+  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
 
 val _ =
   OuterSyntax.command "also" "combine calculation and current facts"
@@ -883,7 +883,7 @@
 
 val _ =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
-    Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
 
 val _ =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
@@ -899,20 +899,20 @@
 
 val _ =
   OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
-    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
+    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
 
 val _ =
   OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
-    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
+    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
 
 val _ =
   OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
-    (opt_modes -- Scan.option SpecParse.xthms1
+    (opt_modes -- Scan.option Parse_Spec.xthms1
       >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
 
 val _ =
   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
-    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
+    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
 
 val _ =
   OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag
diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/Isar/parse_spec.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/parse_spec.ML	Sat May 15 23:32:15 2010 +0200
@@ -0,0 +1,167 @@
+(*  Title:      Pure/Isar/parse_spec.ML
+    Author:     Makarius
+
+Parsers for complex specifications.
+*)
+
+signature PARSE_SPEC =
+sig
+  val attrib: Attrib.src parser
+  val attribs: Attrib.src list parser
+  val opt_attribs: Attrib.src list parser
+  val thm_name: string -> Attrib.binding parser
+  val opt_thm_name: string -> Attrib.binding parser
+  val spec: (Attrib.binding * string) parser
+  val specs: (Attrib.binding * string list) parser
+  val alt_specs: (Attrib.binding * string) list parser
+  val where_alt_specs: (Attrib.binding * string) list parser
+  val xthm: (Facts.ref * Attrib.src list) parser
+  val xthms1: (Facts.ref * Attrib.src list) list parser
+  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+  val constdecl: (binding * string option * mixfix) parser
+  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
+  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 locale_expression: bool -> Expression.expression parser
+  val locale_keyword: string parser
+  val context_element: Element.context parser
+  val statement: (Attrib.binding * (string * string list) list) list parser
+  val general_statement: (Element.context list * Element.statement) parser
+  val statement_keyword: string parser
+end;
+
+structure Parse_Spec: PARSE_SPEC =
+struct
+
+(* theorem specifications *)
+
+val attrib =
+  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
+  >> Args.src;
+
+val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
+val opt_attribs = Scan.optional attribs [];
+
+fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
+
+fun opt_thm_name s =
+  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
+    Attrib.empty_binding;
+
+val spec = opt_thm_name ":" -- Parse.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
+
+val alt_specs =
+  Parse.enum1 "|"
+    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
+
+val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
+
+val xthm =
+  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
+  (Parse.alt_string >> Facts.Fact ||
+    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
+
+val xthms1 = Scan.repeat1 xthm;
+
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
+
+
+(* basic constant specifications *)
+
+val constdecl =
+  Parse.binding --
+    (Parse.where_ >> K (NONE, NoSyn) ||
+      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
+      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
+  >> Parse.triple2;
+
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
+
+
+(* locale and context elements *)
+
+val locale_mixfix =
+  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
+  Parse.mixfix;
+
+val locale_fixes =
+  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+    >> (single o Parse.triple1) ||
+  Parse.params >> map Syntax.no_syn) >> flat;
+
+val locale_insts =
+  Scan.optional
+    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
+  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
+
+local
+
+val loc_element =
+  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
+  Parse.$$$ "constrains" |--
+    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
+    >> Element.Constrains ||
+  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
+    >> Element.Assumes ||
+  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
+    >> Element.Defines ||
+  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
+    >> (curry Element.Notes "");
+
+fun plus1_unless test scan =
+  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
+
+fun prefix mandatory =
+  Parse.name --
+    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
+    Parse.$$$ ":";
+
+val instance = Parse.where_ |--
+  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
+  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
+
+in
+
+val locale_keyword =
+  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
+  Parse.$$$ "defines" || Parse.$$$ "notes";
+
+val class_expr = plus1_unless locale_keyword Parse.xname;
+
+fun locale_expression mandatory =
+  let
+    val expr2 = 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;
+  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
+
+val context_element = Parse.group "context element" loc_element;
+
+end;
+
+
+(* statements *)
+
+val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
+
+val obtain_case =
+  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
+    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+
+val general_statement =
+  statement >> (fn x => ([], Element.Shows x)) ||
+  Scan.repeat context_element --
+   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
+
+val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
+
+end;
+
+(*legacy alias*)
+structure SpecParse = Parse_Spec;
+
diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Sat May 15 23:23:45 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-(*  Title:      Pure/Isar/spec_parse.ML
-    Author:     Makarius
-
-Parsers for complex specifications.
-*)
-
-signature SPEC_PARSE =
-sig
-  val attrib: Attrib.src parser
-  val attribs: Attrib.src list parser
-  val opt_attribs: Attrib.src list parser
-  val thm_name: string -> Attrib.binding parser
-  val opt_thm_name: string -> Attrib.binding parser
-  val spec: (Attrib.binding * string) parser
-  val specs: (Attrib.binding * string list) parser
-  val alt_specs: (Attrib.binding * string) list parser
-  val where_alt_specs: (Attrib.binding * string) list parser
-  val xthm: (Facts.ref * Attrib.src list) parser
-  val xthms1: (Facts.ref * Attrib.src list) list parser
-  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
-  val constdecl: (binding * string option * mixfix) parser
-  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
-  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 locale_expression: bool -> Expression.expression parser
-  val locale_keyword: string parser
-  val context_element: Element.context parser
-  val statement: (Attrib.binding * (string * string list) list) list parser
-  val general_statement: (Element.context list * Element.statement) parser
-  val statement_keyword: string parser
-end;
-
-structure SpecParse: SPEC_PARSE =
-struct
-
-(* theorem specifications *)
-
-val attrib =
-  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
-  >> Args.src;
-
-val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
-val opt_attribs = Scan.optional attribs [];
-
-fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
-
-fun opt_thm_name s =
-  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
-    Attrib.empty_binding;
-
-val spec = opt_thm_name ":" -- Parse.prop;
-val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
-
-val alt_specs =
-  Parse.enum1 "|"
-    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
-
-val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
-
-val xthm =
-  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
-  (Parse.alt_string >> Facts.Fact ||
-    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
-
-val xthms1 = Scan.repeat1 xthm;
-
-val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
-
-
-(* basic constant specifications *)
-
-val constdecl =
-  Parse.binding --
-    (Parse.where_ >> K (NONE, NoSyn) ||
-      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
-      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
-  >> Parse.triple2;
-
-val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
-
-
-(* locale and context elements *)
-
-val locale_mixfix =
-  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
-  Parse.mixfix;
-
-val locale_fixes =
-  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
-    >> (single o Parse.triple1) ||
-  Parse.params >> map Syntax.no_syn) >> flat;
-
-val locale_insts =
-  Scan.optional
-    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
-  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
-
-local
-
-val loc_element =
-  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
-  Parse.$$$ "constrains" |--
-    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
-    >> Element.Constrains ||
-  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
-    >> Element.Assumes ||
-  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
-    >> Element.Defines ||
-  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
-    >> (curry Element.Notes "");
-
-fun plus1_unless test scan =
-  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
-
-fun prefix mandatory =
-  Parse.name --
-    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
-    Parse.$$$ ":";
-
-val instance = Parse.where_ |--
-  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
-  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
-
-in
-
-val locale_keyword =
-  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
-  Parse.$$$ "defines" || Parse.$$$ "notes";
-
-val class_expr = plus1_unless locale_keyword Parse.xname;
-
-fun locale_expression mandatory =
-  let
-    val expr2 = 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;
-  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
-
-val context_element = Parse.group "context element" loc_element;
-
-end;
-
-
-(* statements *)
-
-val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
-
-val obtain_case =
-  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
-    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
-
-val general_statement =
-  statement >> (fn x => ([], Element.Shows x)) ||
-  Scan.repeat context_element --
-   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
-    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
-
-val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
-
-end;
diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat May 15 23:23:45 2010 +0200
+++ b/src/Pure/ROOT.ML	Sat May 15 23:32:15 2010 +0200
@@ -220,7 +220,7 @@
 use "Isar/code.ML";
 
 (*specifications*)
-use "Isar/spec_parse.ML";
+use "Isar/parse_spec.ML";
 use "Isar/spec_rules.ML";
 use "Isar/specification.ML";
 use "Isar/typedecl.ML";