1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat May 15 23:40:00 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 16 00:02:11 2010 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4      |> Symbol.source {do_recover=false}
     1.5      |> OuterLex.source {do_recover=SOME false} lex Position.start
     1.6      |> OuterLex.source_proper
     1.7 -    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
     1.8 +    |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
     1.9      |> Source.exhaust
    1.10    end
    1.11  

     2.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 15 23:40:00 2010 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun May 16 00:02:11 2010 +0200
     2.3 @@ -410,7 +410,7 @@
     2.4  val _ =
     2.5    OuterSyntax.local_theory_to_proof "nominal_primrec"
     2.6      "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
     2.7 -    (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
     2.8 +    (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
     2.9        >> (fn ((((invs, fctxt), fixes), params), specs) =>
    2.10          add_primrec_cmd invs fctxt fixes params specs));
    2.11  

     3.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat May 15 23:40:00 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun May 16 00:02:11 2010 +0200
     3.3 @@ -355,7 +355,7 @@
     3.4       >> (fn opts => fold apply_opt opts default)
     3.5  in
     3.6    fun function_parser default_cfg =
     3.7 -      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
     3.8 +      config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
     3.9  end
    3.10  
    3.11  

     4.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat May 15 23:40:00 2010 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun May 16 00:02:11 2010 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4  
     4.5  val quotdef_parser =
     4.6    Scan.optional quotdef_decl (NONE, NoSyn) -- 
     4.7 -    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
     4.8 +    P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
     4.9  end
    4.10  
    4.11  val _ =

     5.1 --- a/src/HOL/Tools/choice_specification.ML	Sat May 15 23:40:00 2010 +0200
     5.2 +++ b/src/HOL/Tools/choice_specification.ML	Sun May 16 00:02:11 2010 +0200
     5.3 @@ -239,7 +239,7 @@
     5.4  
     5.5  val specification_decl =
     5.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
     5.7 -          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
     5.8 +          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
     5.9  
    5.10  val _ =
    5.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    5.12 @@ -250,7 +250,7 @@
    5.13  val ax_specification_decl =
    5.14      P.name --
    5.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    5.16 -           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
    5.17 +           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
    5.18  
    5.19  val _ =
    5.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal

     6.1 --- a/src/HOL/Tools/inductive.ML	Sat May 15 23:40:00 2010 +0200
     6.2 +++ b/src/HOL/Tools/inductive.ML	Sun May 16 00:02:11 2010 +0200
     6.3 @@ -977,8 +977,8 @@
     6.4  
     6.5  fun gen_ind_decl mk_def coind =
     6.6    P.fixes -- P.for_fixes --
     6.7 -  Scan.optional SpecParse.where_alt_specs [] --
     6.8 -  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
     6.9 +  Scan.optional Parse_Spec.where_alt_specs [] --
    6.10 +  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
    6.11    >> (fn (((preds, params), specs), monos) =>
    6.12        (snd oo gen_add_inductive mk_def true coind preds params specs monos));
    6.13  
    6.14 @@ -995,7 +995,7 @@
    6.15  val _ =
    6.16    OuterSyntax.local_theory "inductive_cases"
    6.17      "create simplified instances of elimination rules (improper)" K.thy_script
    6.18 -    (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
    6.19 +    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
    6.20  
    6.21  end;
    6.22  

     7.1 --- a/src/HOL/Tools/primrec.ML	Sat May 15 23:40:00 2010 +0200
     7.2 +++ b/src/HOL/Tools/primrec.ML	Sun May 16 00:02:11 2010 +0200
     7.3 @@ -315,9 +315,10 @@
     7.4        P.name >> pair false) --| P.$$$ ")")) (false, "");
     7.5  
     7.6  val old_primrec_decl =
     7.7 -  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
     7.8 +  opt_unchecked_name --
     7.9 +    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
    7.10  
    7.11 -val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
    7.12 +val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
    7.13  
    7.14  val _ =
    7.15    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl

     8.1 --- a/src/HOL/Tools/recdef.ML	Sat May 15 23:40:00 2010 +0200
     8.2 +++ b/src/HOL/Tools/recdef.ML	Sun May 16 00:02:11 2010 +0200
     8.3 @@ -298,7 +298,7 @@
     8.4  
     8.5  val recdef_decl =
     8.6    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
     8.7 -  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
     8.8 +  P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
     8.9      -- Scan.option hints
    8.10    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    8.11  
    8.12 @@ -309,7 +309,7 @@
    8.13  
    8.14  val defer_recdef_decl =
    8.15    P.name -- Scan.repeat1 P.prop --
    8.16 -  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
    8.17 +  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
    8.18    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
    8.19  
    8.20  val _ =
    8.21 @@ -319,7 +319,7 @@
    8.22  val _ =
    8.23    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
    8.24      K.thy_goal
    8.25 -    ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
    8.26 +    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
    8.27          Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    8.28        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    8.29  

     9.1 --- a/src/HOLCF/Tools/fixrec.ML	Sat May 15 23:40:00 2010 +0200
     9.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sun May 16 00:02:11 2010 +0200
     9.3 @@ -446,11 +446,11 @@
     9.4  local structure P = OuterParse and K = OuterKeyword in
     9.5  
     9.6  val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
     9.7 -  ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
     9.8 +  ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
     9.9      >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
    9.10  
    9.11  val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
    9.12 -  (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
    9.13 +  (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
    9.14  
    9.15  end;
    9.16  

    10.1 --- a/src/ZF/Tools/datatype_package.ML	Sat May 15 23:40:00 2010 +0200
    10.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun May 16 00:02:11 2010 +0200
    10.3 @@ -431,9 +431,9 @@
    10.4  val datatype_decl =
    10.5    (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
    10.6    P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
    10.7 -  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
    10.8 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
    10.9 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   10.10 +  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
   10.11 +  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
   10.12 +  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   10.13    >> (Toplevel.theory o mk_datatype);
   10.14  
   10.15  val coind_prefix = if coind then "co" else "";

    11.1 --- a/src/ZF/Tools/ind_cases.ML	Sat May 15 23:40:00 2010 +0200
    11.2 +++ b/src/ZF/Tools/ind_cases.ML	Sun May 16 00:02:11 2010 +0200
    11.3 @@ -69,7 +69,7 @@
    11.4  val _ =
    11.5    OuterSyntax.command "inductive_cases"
    11.6      "create simplified instances of elimination rules (improper)" K.thy_script
    11.7 -    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
    11.8 +    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
    11.9        >> (Toplevel.theory o inductive_cases));
   11.10  
   11.11  end;

    12.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 23:40:00 2010 +0200
    12.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun May 16 00:02:11 2010 +0200
    12.3 @@ -191,10 +191,10 @@
    12.4  val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
    12.5  
    12.6  val rep_datatype_decl =
    12.7 -  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
    12.8 -  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
    12.9 -  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
   12.10 -  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   12.11 +  (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
   12.12 +  (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
   12.13 +  (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
   12.14 +  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
   12.15    >> (fn (((x, y), z), w) => rep_datatype x y z w);
   12.16  
   12.17  val _ =

    13.1 --- a/src/ZF/Tools/inductive_package.ML	Sat May 15 23:40:00 2010 +0200
    13.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun May 16 00:02:11 2010 +0200
    13.3 @@ -588,11 +588,11 @@
    13.4    (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
    13.5        ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
    13.6    (P.$$$ "intros" |--
    13.7 -    P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
    13.8 -  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
    13.9 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! SpecParse.xthms1) [] --
   13.10 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
   13.11 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   13.12 +    P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
   13.13 +  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
   13.14 +  Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
   13.15 +  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
   13.16 +  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   13.17    >> (Toplevel.theory o mk_ind);
   13.18  
   13.19  val _ = OuterSyntax.command (co_prefix ^ "inductive")

    14.1 --- a/src/ZF/Tools/primrec_package.ML	Sat May 15 23:40:00 2010 +0200
    14.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun May 16 00:02:11 2010 +0200
    14.3 @@ -198,7 +198,7 @@
    14.4  
    14.5  val _ =
    14.6    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    14.7 -    (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
    14.8 +    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
    14.9        >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
   14.10  
   14.11  end;