# HG changeset patch
# User wenzelm
# Date 1273960931 -7200
# Node ID ef698bd61057c3ee67607b32ae8267fcc53ae1b6
# Parent  2af1ad9aa1a3d2ead5cca8e7d4567a01d797a48e
prefer structure Parse_Spec;

diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 16 00:02:11 2010 +0200
@@ -337,7 +337,7 @@
     |> Symbol.source {do_recover=false}
     |> OuterLex.source {do_recover=SOME false} lex Position.start
     |> OuterLex.source_proper
-    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+    |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
     |> Source.exhaust
   end
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun May 16 00:02:11 2010 +0200
@@ -410,7 +410,7 @@
 val _ =
   OuterSyntax.local_theory_to_proof "nominal_primrec"
     "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
-    (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
+    (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
       >> (fn ((((invs, fctxt), fixes), params), specs) =>
         add_primrec_cmd invs fctxt fixes params specs));
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun May 16 00:02:11 2010 +0200
@@ -355,7 +355,7 @@
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
-      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
+      config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
 end
 
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun May 16 00:02:11 2010 +0200
@@ -99,7 +99,7 @@
 
 val quotdef_parser =
   Scan.optional quotdef_decl (NONE, NoSyn) -- 
-    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
+    P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
 end
 
 val _ =
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sun May 16 00:02:11 2010 +0200
@@ -239,7 +239,7 @@
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
+          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
 
 val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -250,7 +250,7 @@
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
+           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
 
 val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun May 16 00:02:11 2010 +0200
@@ -977,8 +977,8 @@
 
 fun gen_ind_decl mk_def coind =
   P.fixes -- P.for_fixes --
-  Scan.optional SpecParse.where_alt_specs [] --
-  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
+  Scan.optional Parse_Spec.where_alt_specs [] --
+  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd oo gen_add_inductive mk_def true coind preds params specs monos));
 
@@ -995,7 +995,7 @@
 val _ =
   OuterSyntax.local_theory "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
+    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
 
 end;
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Sun May 16 00:02:11 2010 +0200
@@ -315,9 +315,10 @@
       P.name >> pair false) --| P.$$$ ")")) (false, "");
 
 val old_primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
+  opt_unchecked_name --
+    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
 
-val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
+val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
 
 val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/recdef.ML	Sun May 16 00:02:11 2010 +0200
@@ -298,7 +298,7 @@
 
 val recdef_decl =
   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
-  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+  P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
     -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
@@ -309,7 +309,7 @@
 
 val defer_recdef_decl =
   P.name -- Scan.repeat1 P.prop --
-  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
+  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
@@ -319,7 +319,7 @@
 val _ =
   OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
     K.thy_goal
-    ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
+    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
         Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Sun May 16 00:02:11 2010 +0200
@@ -446,11 +446,11 @@
 local structure P = OuterParse and K = OuterKeyword in
 
 val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
-  ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
+  ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
     >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
 
 val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
-  (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
+  (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
 
 end;
 
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun May 16 00:02:11 2010 +0200
@@ -431,9 +431,9 @@
 val datatype_decl =
   (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
-  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
-  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
+  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_datatype);
 
 val coind_prefix = if coind then "co" else "";
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Sun May 16 00:02:11 2010 +0200
@@ -69,7 +69,7 @@
 val _ =
   OuterSyntax.command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
       >> (Toplevel.theory o inductive_cases));
 
 end;
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sun May 16 00:02:11 2010 +0200
@@ -191,10 +191,10 @@
 val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
 
 val rep_datatype_decl =
-  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
-  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
-  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
-  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
+  (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
+  (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
+  (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
+  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
   >> (fn (((x, y), z), w) => rep_datatype x y z w);
 
 val _ =
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sun May 16 00:02:11 2010 +0200
@@ -588,11 +588,11 @@
   (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
       ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
   (P.$$$ "intros" |--
-    P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
-  Scan.optional (P.$$$ "con_defs" |-- P.!!! SpecParse.xthms1) [] --
-  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
-  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
+    P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
+  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_ind);
 
 val _ = OuterSyntax.command (co_prefix ^ "inductive")
diff -r 2af1ad9aa1a3 -r ef698bd61057 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sun May 16 00:02:11 2010 +0200
@@ -198,7 +198,7 @@
 
 val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
       >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
 
 end;