src/Pure/Pure.thy
changeset 62969 9f394a16c557
parent 62944 3ee643c5ed00
child 63039 1a20fd9cf281
     1.1 --- a/src/Pure/Pure.thy	Wed Apr 13 17:00:02 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Wed Apr 13 18:01:05 2016 +0200
     1.3 @@ -280,7 +280,7 @@
     1.4  
     1.5  val trans_pat =
     1.6    Scan.optional
     1.7 -    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
     1.8 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
     1.9      -- Parse.inner_syntax Parse.string;
    1.10  
    1.11  fun trans_arrow toks =
    1.12 @@ -403,7 +403,7 @@
    1.13  
    1.14  val _ =
    1.15    Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
    1.16 -    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
    1.17 +    (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
    1.18        >> (fn (facts, fixes) =>
    1.19            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
    1.20  
    1.21 @@ -442,7 +442,7 @@
    1.22  
    1.23  val _ =
    1.24    hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
    1.25 -    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
    1.26 +    (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
    1.27  
    1.28  in end\<close>
    1.29  
    1.30 @@ -454,18 +454,18 @@
    1.31  
    1.32  val _ =
    1.33    Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
    1.34 -    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
    1.35 +    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
    1.36        >> (uncurry Bundle.bundle_cmd));
    1.37  
    1.38  val _ =
    1.39    Outer_Syntax.command @{command_keyword include}
    1.40      "include declarations from bundle in proof body"
    1.41 -    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
    1.42 +    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
    1.43  
    1.44  val _ =
    1.45    Outer_Syntax.command @{command_keyword including}
    1.46      "include declarations from bundle in goal refinement"
    1.47 -    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
    1.48 +    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
    1.49  
    1.50  val _ =
    1.51    Outer_Syntax.command @{command_keyword print_bundles}
    1.52 @@ -484,7 +484,7 @@
    1.53  
    1.54  val _ =
    1.55    Outer_Syntax.command @{command_keyword context} "begin local theory context"
    1.56 -    ((Parse.position Parse.xname >> (fn name =>
    1.57 +    ((Parse.position Parse.name >> (fn name =>
    1.58          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
    1.59        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
    1.60          >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
    1.61 @@ -550,7 +550,7 @@
    1.62  val _ =
    1.63    Outer_Syntax.command @{command_keyword sublocale}
    1.64      "prove sublocale relation between a locale and a locale expression"
    1.65 -    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
    1.66 +    ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
    1.67        interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
    1.68          Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
    1.69      || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
    1.70 @@ -684,7 +684,7 @@
    1.71  ML \<open>
    1.72  local
    1.73  
    1.74 -val facts = Parse.and_list1 Parse.xthms1;
    1.75 +val facts = Parse.and_list1 Parse.thms1;
    1.76  
    1.77  val _ =
    1.78    Outer_Syntax.command @{command_keyword then} "forward chaining"
    1.79 @@ -773,9 +773,9 @@
    1.80    Outer_Syntax.command @{command_keyword case} "invoke local context"
    1.81      (Parse_Spec.opt_thm_name ":" --
    1.82        (@{keyword "("} |--
    1.83 -        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
    1.84 +        Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
    1.85            --| @{keyword ")"}) ||
    1.86 -        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
    1.87 +        Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
    1.88  
    1.89  in end\<close>
    1.90  
    1.91 @@ -906,7 +906,7 @@
    1.92  local
    1.93  
    1.94  val calculation_args =
    1.95 -  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
    1.96 +  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
    1.97  
    1.98  val _ =
    1.99    Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
   1.100 @@ -956,7 +956,7 @@
   1.101  local
   1.102  
   1.103  val opt_modes =
   1.104 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   1.105 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
   1.106  
   1.107  val _ =
   1.108    Outer_Syntax.command @{command_keyword help}
   1.109 @@ -1025,13 +1025,13 @@
   1.110  val _ =
   1.111    Outer_Syntax.command @{command_keyword print_locale}
   1.112      "print locale of this theory"
   1.113 -    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   1.114 +    (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
   1.115        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
   1.116  
   1.117  val _ =
   1.118    Outer_Syntax.command @{command_keyword print_interps}
   1.119      "print interpretations of locale for this theory or proof context"
   1.120 -    (Parse.position Parse.xname >> (fn name =>
   1.121 +    (Parse.position Parse.name >> (fn name =>
   1.122        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
   1.123  
   1.124  val _ =
   1.125 @@ -1100,19 +1100,19 @@
   1.126  val _ =
   1.127    Outer_Syntax.command @{command_keyword print_statement}
   1.128      "print theorems as long statements"
   1.129 -    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
   1.130 +    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
   1.131  
   1.132  val _ =
   1.133    Outer_Syntax.command @{command_keyword thm} "print theorems"
   1.134 -    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
   1.135 +    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
   1.136  
   1.137  val _ =
   1.138    Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
   1.139 -    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
   1.140 +    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
   1.141  
   1.142  val _ =
   1.143    Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
   1.144 -    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
   1.145 +    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
   1.146  
   1.147  val _ =
   1.148    Outer_Syntax.command @{command_keyword prop} "read and print proposition"
   1.149 @@ -1156,8 +1156,8 @@
   1.150  local
   1.151  
   1.152  val theory_bounds =
   1.153 -  Parse.position Parse.theory_xname >> single ||
   1.154 -  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   1.155 +  Parse.position Parse.theory_name >> single ||
   1.156 +  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
   1.157  
   1.158  val _ =
   1.159    Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
   1.160 @@ -1177,14 +1177,14 @@
   1.161  
   1.162  val _ =
   1.163    Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
   1.164 -    (Parse.xthms1 >> (fn args =>
   1.165 +    (Parse.thms1 >> (fn args =>
   1.166        Toplevel.keep (fn st =>
   1.167          Thm_Deps.thm_deps (Toplevel.theory_of st)
   1.168            (Attrib.eval_thms (Toplevel.context_of st) args))));
   1.169  
   1.170  
   1.171  val thy_names =
   1.172 -  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   1.173 +  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
   1.174  
   1.175  val _ =
   1.176    Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   1.177 @@ -1260,7 +1260,7 @@
   1.178  val _ =
   1.179    Outer_Syntax.command @{command_keyword realizers}
   1.180      "specify realizers for primitive axioms / theorems, together with correctness proof"
   1.181 -    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
   1.182 +    (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
   1.183       (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
   1.184         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
   1.185  
   1.186 @@ -1276,7 +1276,7 @@
   1.187  
   1.188  val _ =
   1.189    Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
   1.190 -    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   1.191 +    (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   1.192        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
   1.193  
   1.194  in end\<close>