# 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.$$$ "\" || 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.$$$ "\" || 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;