merged
authorwenzelm
Mon Apr 06 23:24:45 2015 +0200 (2015-04-06)
changeset 59941bafba7916d5e
parent 59928 b9b7f913a19a
parent 59940 087d81f5213e
child 59942 6a3098313acf
merged
     1.1 --- a/NEWS	Mon Apr 06 15:23:50 2015 +0200
     1.2 +++ b/NEWS	Mon Apr 06 23:24:45 2015 +0200
     1.3 @@ -6,9 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Local theory specifications may have a 'private' modifier to restrict
     1.8 -name space accesses to the current local scope, as delimited by "context
     1.9 -begin ... end". For example, this works like this:
    1.10 +* Local theory specification commands may have a 'private' or
    1.11 +'restricted' modifier to limit name space accesses to the local scope,
    1.12 +as provided by some "context begin ... end" block. For example:
    1.13  
    1.14    context
    1.15    begin
    1.16 @@ -407,6 +407,10 @@
    1.17  * Goal.prove_multi is superseded by the fully general Goal.prove_common,
    1.18  which also allows to specify a fork priority.
    1.19  
    1.20 +* Antiquotation @{command_spec "COMMAND"} is superseded by
    1.21 +@{command_keyword COMMAND} (usually without quotes and with PIDE
    1.22 +markup). Minor INCOMPATIBILITY.
    1.23 +
    1.24  
    1.25  *** System ***
    1.26  
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 15:23:50 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 23:24:45 2015 +0200
     2.3 @@ -471,7 +471,7 @@
     2.4    \end{matharray}
     2.5  
     2.6    @{rail \<open>
     2.7 -    'rail' (@{syntax string} | @{syntax cartouche})
     2.8 +    'rail' @{syntax text}
     2.9    \<close>}
    2.10  
    2.11    The @{antiquotation rail} antiquotation allows to include syntax
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 15:23:50 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 23:24:45 2015 +0200
     3.3 @@ -115,6 +115,7 @@
     3.4      @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     3.5      @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     3.6      @{keyword_def "private"} \\
     3.7 +    @{keyword_def "restricted"} \\
     3.8    \end{matharray}
     3.9  
    3.10    A local theory target is a specification context that is managed
    3.11 @@ -161,12 +162,16 @@
    3.12    (global) "end"} has a different meaning: it concludes the theory
    3.13    itself (\secref{sec:begin-thy}).
    3.14    
    3.15 -  \item @{keyword "private"} may be given as a modifier to any local theory
    3.16 -  command (before the command keyword). This limits name space accesses to
    3.17 -  the current local scope, as determined by the enclosing @{command
    3.18 -  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
    3.19 -  global theory nor a locale target have such a local scope by themselves:
    3.20 -  an extra unnamed context is required to use @{keyword "private"} here.
    3.21 +  \item @{keyword "private"} or @{keyword "restricted"} may be given as
    3.22 +  modifiers before any local theory command. This limits name space accesses
    3.23 +  to the local scope, as determined by the enclosing @{command
    3.24 +  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
    3.25 +  scope, a @{keyword "private"} name is inaccessible, and a @{keyword
    3.26 +  "restricted"} name is only accessible with additional qualification.
    3.27 +
    3.28 +  Neither a global @{command theory} nor a @{command locale} target provides
    3.29 +  a local scope by itself: an extra unnamed context is required to use
    3.30 +  @{keyword "private"} or @{keyword "restricted"} here.
    3.31  
    3.32    \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
    3.33    theory command specifies an immediate target, e.g.\ ``@{command
     4.1 --- a/src/FOL/FOL.thy	Mon Apr 06 15:23:50 2015 +0200
     4.2 +++ b/src/FOL/FOL.thy	Mon Apr 06 23:24:45 2015 +0200
     4.3 @@ -384,10 +384,13 @@
     4.4  
     4.5  text {* Proper handling of non-atomic rule statements. *}
     4.6  
     4.7 -definition "induct_forall(P) == \<forall>x. P(x)"
     4.8 -definition "induct_implies(A, B) == A \<longrightarrow> B"
     4.9 -definition "induct_equal(x, y) == x = y"
    4.10 -definition "induct_conj(A, B) == A \<and> B"
    4.11 +context
    4.12 +begin
    4.13 +
    4.14 +restricted definition "induct_forall(P) == \<forall>x. P(x)"
    4.15 +restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
    4.16 +restricted definition "induct_equal(x, y) == x = y"
    4.17 +restricted definition "induct_conj(A, B) == A \<and> B"
    4.18  
    4.19  lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
    4.20    unfolding atomize_all induct_forall_def .
    4.21 @@ -406,9 +409,6 @@
    4.22  lemmas induct_rulify_fallback =
    4.23    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    4.24  
    4.25 -hide_const induct_forall induct_implies induct_equal induct_conj
    4.26 -
    4.27 -
    4.28  text {* Method setup. *}
    4.29  
    4.30  ML_file "~~/src/Tools/induct.ML"
    4.31 @@ -427,6 +427,8 @@
    4.32  
    4.33  declare case_split [cases type: o]
    4.34  
    4.35 +end
    4.36 +
    4.37  ML_file "~~/src/Tools/case_product.ML"
    4.38  
    4.39  
     5.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 15:23:50 2015 +0200
     5.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 23:24:45 2015 +0200
     5.3 @@ -244,7 +244,7 @@
     5.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     5.8 +  Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
     5.9      (opt_modes -- Parse.term
    5.10        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
    5.11  
     6.1 --- a/src/HOL/Extraction.thy	Mon Apr 06 15:23:50 2015 +0200
     6.2 +++ b/src/HOL/Extraction.thy	Mon Apr 06 23:24:45 2015 +0200
     6.3 @@ -34,8 +34,8 @@
     6.4    True_implies_equals TrueE
     6.5  
     6.6  lemmas [extraction_expand_def] =
     6.7 -  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     6.8 -  induct_true_def induct_false_def
     6.9 +  HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
    6.10 +  HOL.induct_true_def HOL.induct_false_def
    6.11  
    6.12  datatype (plugins only: code extraction) sumbool = Left | Right
    6.13  
     7.1 --- a/src/HOL/HOL.thy	Mon Apr 06 15:23:50 2015 +0200
     7.2 +++ b/src/HOL/HOL.thy	Mon Apr 06 23:24:45 2015 +0200
     7.3 @@ -1365,44 +1365,35 @@
     7.4  subsubsection {* Generic cases and induction *}
     7.5  
     7.6  text {* Rule projections: *}
     7.7 -
     7.8  ML {*
     7.9  structure Project_Rule = Project_Rule
    7.10  (
    7.11    val conjunct1 = @{thm conjunct1}
    7.12    val conjunct2 = @{thm conjunct2}
    7.13    val mp = @{thm mp}
    7.14 -)
    7.15 +);
    7.16  *}
    7.17  
    7.18 -definition induct_forall where
    7.19 -  "induct_forall P == \<forall>x. P x"
    7.20 -
    7.21 -definition induct_implies where
    7.22 -  "induct_implies A B == A \<longrightarrow> B"
    7.23 -
    7.24 -definition induct_equal where
    7.25 -  "induct_equal x y == x = y"
    7.26 +context
    7.27 +begin
    7.28  
    7.29 -definition induct_conj where
    7.30 -  "induct_conj A B == A \<and> B"
    7.31 +restricted definition "induct_forall P \<equiv> \<forall>x. P x"
    7.32 +restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    7.33 +restricted definition "induct_equal x y \<equiv> x = y"
    7.34 +restricted definition "induct_conj A B \<equiv> A \<and> B"
    7.35 +restricted definition "induct_true \<equiv> True"
    7.36 +restricted definition "induct_false \<equiv> False"
    7.37  
    7.38 -definition induct_true where
    7.39 -  "induct_true == True"
    7.40 -
    7.41 -definition induct_false where
    7.42 -  "induct_false == False"
    7.43 -
    7.44 -lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
    7.45 +lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    7.46    by (unfold atomize_all induct_forall_def)
    7.47  
    7.48 -lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
    7.49 +lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
    7.50    by (unfold atomize_imp induct_implies_def)
    7.51  
    7.52 -lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
    7.53 +lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
    7.54    by (unfold atomize_eq induct_equal_def)
    7.55  
    7.56 -lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
    7.57 +lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
    7.58    by (unfold atomize_conj induct_conj_def)
    7.59  
    7.60  lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
    7.61 @@ -1413,7 +1404,6 @@
    7.62    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    7.63    induct_true_def induct_false_def
    7.64  
    7.65 -
    7.66  lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
    7.67      induct_conj (induct_forall A) (induct_forall B)"
    7.68    by (unfold induct_forall_def induct_conj_def) iprover
    7.69 @@ -1422,13 +1412,15 @@
    7.70      induct_conj (induct_implies C A) (induct_implies C B)"
    7.71    by (unfold induct_implies_def induct_conj_def) iprover
    7.72  
    7.73 -lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
    7.74 +lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
    7.75  proof
    7.76 -  assume r: "induct_conj A B ==> PROP C" and A B
    7.77 -  show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
    7.78 +  assume r: "induct_conj A B \<Longrightarrow> PROP C"
    7.79 +  assume ab: A B
    7.80 +  show "PROP C" by (rule r) (simp add: induct_conj_def ab)
    7.81  next
    7.82 -  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
    7.83 -  show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
    7.84 +  assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
    7.85 +  assume ab: "induct_conj A B"
    7.86 +  show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
    7.87  qed
    7.88  
    7.89  lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
    7.90 @@ -1455,8 +1447,8 @@
    7.91  
    7.92  ML_file "~~/src/Tools/induction.ML"
    7.93  
    7.94 -setup {*
    7.95 -  Context.theory_map (Induct.map_simpset (fn ss => ss
    7.96 +declaration {*
    7.97 +  fn _ => Induct.map_simpset (fn ss => ss
    7.98      addsimprocs
    7.99        [Simplifier.simproc_global @{theory} "swap_induct_false"
   7.100           ["induct_false ==> PROP P ==> PROP Q"]
   7.101 @@ -1479,60 +1471,62 @@
   7.102                | _ => NONE))]
   7.103      |> Simplifier.set_mksimps (fn ctxt =>
   7.104          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
   7.105 -        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
   7.106 +        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
   7.107  *}
   7.108  
   7.109  text {* Pre-simplification of induction and cases rules *}
   7.110  
   7.111 -lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
   7.112 +lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   7.113    unfolding induct_equal_def
   7.114  proof
   7.115 -  assume R: "!!x. x = t ==> PROP P x"
   7.116 -  show "PROP P t" by (rule R [OF refl])
   7.117 +  assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
   7.118 +  show "PROP P t" by (rule r [OF refl])
   7.119  next
   7.120 -  fix x assume "PROP P t" "x = t"
   7.121 +  fix x
   7.122 +  assume "PROP P t" "x = t"
   7.123    then show "PROP P x" by simp
   7.124  qed
   7.125  
   7.126 -lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
   7.127 +lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   7.128    unfolding induct_equal_def
   7.129  proof
   7.130 -  assume R: "!!x. t = x ==> PROP P x"
   7.131 -  show "PROP P t" by (rule R [OF refl])
   7.132 +  assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
   7.133 +  show "PROP P t" by (rule r [OF refl])
   7.134  next
   7.135 -  fix x assume "PROP P t" "t = x"
   7.136 +  fix x
   7.137 +  assume "PROP P t" "t = x"
   7.138    then show "PROP P x" by simp
   7.139  qed
   7.140  
   7.141 -lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
   7.142 +lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
   7.143    unfolding induct_false_def induct_true_def
   7.144    by (iprover intro: equal_intr_rule)
   7.145  
   7.146 -lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
   7.147 +lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
   7.148    unfolding induct_true_def
   7.149  proof
   7.150 -  assume R: "True \<Longrightarrow> PROP P"
   7.151 -  from TrueI show "PROP P" by (rule R)
   7.152 +  assume "True \<Longrightarrow> PROP P"
   7.153 +  then show "PROP P" using TrueI .
   7.154  next
   7.155    assume "PROP P"
   7.156    then show "PROP P" .
   7.157  qed
   7.158  
   7.159 -lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
   7.160 +lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
   7.161    unfolding induct_true_def
   7.162    by (iprover intro: equal_intr_rule)
   7.163  
   7.164 -lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
   7.165 +lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
   7.166    unfolding induct_true_def
   7.167    by (iprover intro: equal_intr_rule)
   7.168  
   7.169 -lemma [induct_simp]: "induct_implies induct_true P == P"
   7.170 +lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
   7.171    by (simp add: induct_implies_def induct_true_def)
   7.172  
   7.173 -lemma [induct_simp]: "(x = x) = True"
   7.174 +lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   7.175    by (rule simp_thms)
   7.176  
   7.177 -hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
   7.178 +end
   7.179  
   7.180  ML_file "~~/src/Tools/induct_tacs.ML"
   7.181  
     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Apr 06 15:23:50 2015 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Apr 06 23:24:45 2015 +0200
     8.3 @@ -261,7 +261,7 @@
     8.4    end
     8.5  
     8.6  val _ =
     8.7 -  Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
     8.8 +  Outer_Syntax.command @{command_keyword domain} "define recursive domains (HOLCF)"
     8.9      (domains_decl >> (Toplevel.theory o mk_domain))
    8.10  
    8.11  end
     9.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Apr 06 15:23:50 2015 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Apr 06 23:24:45 2015 +0200
     9.3 @@ -755,7 +755,7 @@
     9.4  in
     9.5  
     9.6  val _ =
     9.7 -  Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
     9.8 +  Outer_Syntax.command @{command_keyword domain_isomorphism} "define domain isomorphisms (HOLCF)"
     9.9      (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
    9.10  
    9.11  end
    10.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Apr 06 15:23:50 2015 +0200
    10.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Apr 06 23:24:45 2015 +0200
    10.3 @@ -332,12 +332,12 @@
    10.4      ((t, args, mx), A, morphs)
    10.5  
    10.6  val _ =
    10.7 -  Outer_Syntax.command @{command_spec "pcpodef"}
    10.8 +  Outer_Syntax.command @{command_keyword pcpodef}
    10.9      "HOLCF type definition (requires admissibility proof)"
   10.10      (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
   10.11  
   10.12  val _ =
   10.13 -  Outer_Syntax.command @{command_spec "cpodef"}
   10.14 +  Outer_Syntax.command @{command_keyword cpodef}
   10.15      "HOLCF type definition (requires admissibility proof)"
   10.16      (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
   10.17  
    11.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Mon Apr 06 15:23:50 2015 +0200
    11.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon Apr 06 23:24:45 2015 +0200
    11.3 @@ -209,7 +209,7 @@
    11.4    domaindef_cmd ((t, args, mx), A, morphs)
    11.5  
    11.6  val _ =
    11.7 -  Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
    11.8 +  Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
    11.9      (domaindef_decl >> (Toplevel.theory o mk_domaindef))
   11.10  
   11.11  end
    12.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Apr 06 15:23:50 2015 +0200
    12.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Apr 06 23:24:45 2015 +0200
    12.3 @@ -399,7 +399,7 @@
    12.4    in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
    12.5  
    12.6  val _ =
    12.7 -  Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
    12.8 +  Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
    12.9      (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
   12.10        >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
   12.11  
    13.1 --- a/src/HOL/Import/import_data.ML	Mon Apr 06 15:23:50 2015 +0200
    13.2 +++ b/src/HOL/Import/import_data.ML	Mon Apr 06 23:24:45 2015 +0200
    13.3 @@ -117,13 +117,13 @@
    13.4    "declare a type_definition theorem as a map for an imported type with abs and rep")
    13.5  
    13.6  val _ =
    13.7 -  Outer_Syntax.command @{command_spec "import_type_map"}
    13.8 +  Outer_Syntax.command @{command_keyword import_type_map}
    13.9      "map external type name to existing Isabelle/HOL type name"
   13.10      ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
   13.11        (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
   13.12  
   13.13  val _ =
   13.14 -  Outer_Syntax.command @{command_spec "import_const_map"}
   13.15 +  Outer_Syntax.command @{command_keyword import_const_map}
   13.16      "map external const name to existing Isabelle/HOL const name"
   13.17      ((Parse.name --| @{keyword ":"}) -- Parse.const >>
   13.18        (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
    14.1 --- a/src/HOL/Import/import_rule.ML	Mon Apr 06 15:23:50 2015 +0200
    14.2 +++ b/src/HOL/Import/import_rule.ML	Mon Apr 06 23:24:45 2015 +0200
    14.3 @@ -444,7 +444,7 @@
    14.4  fun process_file path thy =
    14.5    (thy, init_state) |> File.fold_lines process_line path |> fst
    14.6  
    14.7 -val _ = Outer_Syntax.command @{command_spec "import_file"}
    14.8 +val _ = Outer_Syntax.command @{command_keyword import_file}
    14.9    "import a recorded proof file"
   14.10    (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
   14.11  
    15.1 --- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Apr 06 15:23:50 2015 +0200
    15.2 +++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Apr 06 23:24:45 2015 +0200
    15.3 @@ -246,7 +246,7 @@
    15.4    end
    15.5  
    15.6  val _ =
    15.7 -  Outer_Syntax.command @{command_spec "old_smt_status"}
    15.8 +  Outer_Syntax.command @{command_keyword old_smt_status}
    15.9      "show the available SMT solvers, the currently selected SMT solver, \
   15.10      \and the values of SMT configuration options"
   15.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    16.1 --- a/src/HOL/Library/bnf_axiomatization.ML	Mon Apr 06 15:23:50 2015 +0200
    16.2 +++ b/src/HOL/Library/bnf_axiomatization.ML	Mon Apr 06 23:24:45 2015 +0200
    16.3 @@ -118,7 +118,7 @@
    16.4    parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
    16.5  
    16.6  val _ =
    16.7 -  Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
    16.8 +  Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
    16.9      (parse_bnf_axiomatization >> 
   16.10        (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
   16.11           bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
    17.1 --- a/src/HOL/Library/code_test.ML	Mon Apr 06 15:23:50 2015 +0200
    17.2 +++ b/src/HOL/Library/code_test.ML	Mon Apr 06 23:24:45 2015 +0200
    17.3 @@ -567,7 +567,7 @@
    17.4  val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
    17.5  
    17.6  val _ = 
    17.7 -  Outer_Syntax.command @{command_spec "test_code"}
    17.8 +  Outer_Syntax.command @{command_keyword test_code}
    17.9      "compile test cases to target languages, execute them and report results"
   17.10        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   17.11  
    18.1 --- a/src/HOL/Library/refute.ML	Mon Apr 06 15:23:50 2015 +0200
    18.2 +++ b/src/HOL/Library/refute.ML	Mon Apr 06 23:24:45 2015 +0200
    18.3 @@ -2965,7 +2965,7 @@
    18.4  (* 'refute' command *)
    18.5  
    18.6  val _ =
    18.7 -  Outer_Syntax.command @{command_spec "refute"}
    18.8 +  Outer_Syntax.command @{command_keyword refute}
    18.9      "try to find a model that refutes a given subgoal"
   18.10      (scan_parms -- Scan.optional Parse.nat 1 >>
   18.11        (fn (parms, i) =>
   18.12 @@ -2980,7 +2980,7 @@
   18.13  (* 'refute_params' command *)
   18.14  
   18.15  val _ =
   18.16 -  Outer_Syntax.command @{command_spec "refute_params"}
   18.17 +  Outer_Syntax.command @{command_keyword refute_params}
   18.18      "show/store default parameters for the 'refute' command"
   18.19      (scan_parms >> (fn parms =>
   18.20        Toplevel.theory (fn thy =>
    19.1 --- a/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 15:23:50 2015 +0200
    19.2 +++ b/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 23:24:45 2015 +0200
    19.3 @@ -219,7 +219,7 @@
    19.4    end
    19.5  
    19.6  val _ =
    19.7 -  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
    19.8 +  Outer_Syntax.local_theory @{command_keyword case_of_simps}
    19.9      "turn a list of equations into a case expression"
   19.10      (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
   19.11  
   19.12 @@ -227,7 +227,7 @@
   19.13    Parse.xthms1 --| @{keyword ")"}
   19.14  
   19.15  val _ =
   19.16 -  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
   19.17 +  Outer_Syntax.local_theory @{command_keyword simps_of_case}
   19.18      "perform case split on rule"
   19.19      (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
   19.20        Scan.optional parse_splits [] >> simps_of_case_cmd)
    20.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 15:23:50 2015 +0200
    20.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 23:24:45 2015 +0200
    20.3 @@ -247,10 +247,10 @@
    20.4    end
    20.5  
    20.6  val forbidden_mutant_constnames =
    20.7 - ["HOL.induct_equal",
    20.8 -  "HOL.induct_implies",
    20.9 -  "HOL.induct_conj",
   20.10 -  "HOL.induct_forall",
   20.11 +[@{const_name HOL.induct_equal},
   20.12 + @{const_name HOL.induct_implies},
   20.13 + @{const_name HOL.induct_conj},
   20.14 + @{const_name HOL.induct_forall},
   20.15   @{const_name undefined},
   20.16   @{const_name default},
   20.17   @{const_name Pure.dummy_pattern},
    21.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Apr 06 15:23:50 2015 +0200
    21.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 06 23:24:45 2015 +0200
    21.3 @@ -3563,7 +3563,7 @@
    21.4    (* connectives *)
    21.5    if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
    21.6    true_eqvt false_eqvt
    21.7 -  imp_eqvt [folded induct_implies_def]
    21.8 +  imp_eqvt [folded HOL.induct_implies_def]
    21.9    
   21.10    (* datatypes *)
   21.11    perm_unit.simps
    22.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 15:23:50 2015 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 23:24:45 2015 +0200
    22.3 @@ -28,7 +28,7 @@
    22.4  val finite_emptyI = @{thm "finite.emptyI"};
    22.5  val Collect_const = @{thm "Collect_const"};
    22.6  
    22.7 -val inductive_forall_def = @{thm "induct_forall_def"};
    22.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
    22.9  
   22.10  
   22.11  (* theory data *)
   22.12 @@ -1018,7 +1018,7 @@
   22.13  (* syntax und parsing *)
   22.14  
   22.15  val _ =
   22.16 -  Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
   22.17 +  Outer_Syntax.command @{command_keyword atom_decl} "declare new kinds of atoms"
   22.18      (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
   22.19  
   22.20  end;
    23.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 06 15:23:50 2015 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 06 23:24:45 2015 +0200
    23.3 @@ -2074,7 +2074,7 @@
    23.4  val nominal_datatype_cmd = gen_nominal_datatype Old_Datatype.read_specs;
    23.5  
    23.6  val _ =
    23.7 -  Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
    23.8 +  Outer_Syntax.command @{command_keyword nominal_datatype} "define nominal datatypes"
    23.9      (Parse.and_list1 Old_Datatype.spec_cmd >>
   23.10        (Toplevel.theory o nominal_datatype_cmd Old_Datatype_Aux.default_config));
   23.11  
    24.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 15:23:50 2015 +0200
    24.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 23:24:45 2015 +0200
    24.3 @@ -14,7 +14,7 @@
    24.4  structure NominalInductive : NOMINAL_INDUCTIVE =
    24.5  struct
    24.6  
    24.7 -val inductive_forall_def = @{thm induct_forall_def};
    24.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
    24.9  val inductive_atomize = @{thms induct_atomize};
   24.10  val inductive_rulify = @{thms induct_rulify};
   24.11  
   24.12 @@ -671,14 +671,14 @@
   24.13  (* outer syntax *)
   24.14  
   24.15  val _ =
   24.16 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
   24.17 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
   24.18      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
   24.19      (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
   24.20        (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
   24.21          prove_strong_ind name avoids));
   24.22  
   24.23  val _ =
   24.24 -  Outer_Syntax.local_theory @{command_spec "equivariance"}
   24.25 +  Outer_Syntax.local_theory @{command_keyword equivariance}
   24.26      "prove equivariance for inductive predicate involving nominal datatypes"
   24.27      (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
   24.28        (fn (name, atoms) => prove_eqvt name atoms));
    25.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 15:23:50 2015 +0200
    25.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 23:24:45 2015 +0200
    25.3 @@ -15,7 +15,7 @@
    25.4  structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
    25.5  struct
    25.6  
    25.7 -val inductive_forall_def = @{thm induct_forall_def};
    25.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
    25.9  val inductive_atomize = @{thms induct_atomize};
   25.10  val inductive_rulify = @{thms induct_rulify};
   25.11  
   25.12 @@ -483,7 +483,7 @@
   25.13  (* outer syntax *)
   25.14  
   25.15  val _ =
   25.16 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
   25.17 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
   25.18      "prove strong induction theorem for inductive predicate involving nominal datatypes"
   25.19      (Parse.xname -- 
   25.20       Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
    26.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Mon Apr 06 15:23:50 2015 +0200
    26.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Apr 06 23:24:45 2015 +0200
    26.3 @@ -403,7 +403,7 @@
    26.4    Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
    26.5  
    26.6  val _ =
    26.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
    26.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
    26.9      "define primitive recursive functions on nominal datatypes"
   26.10      (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
   26.11        >> (fn ((((invs, fctxt), fixes), params), specs) =>
    27.1 --- a/src/HOL/Orderings.thy	Mon Apr 06 15:23:50 2015 +0200
    27.2 +++ b/src/HOL/Orderings.thy	Mon Apr 06 23:24:45 2015 +0200
    27.3 @@ -439,7 +439,7 @@
    27.4    end;
    27.5  
    27.6  val _ =
    27.7 -  Outer_Syntax.command @{command_spec "print_orders"}
    27.8 +  Outer_Syntax.command @{command_keyword print_orders}
    27.9      "print order structures available to transitivity reasoner"
   27.10      (Scan.succeed (Toplevel.unknown_context o
   27.11        Toplevel.keep (print_structures o Toplevel.context_of)));
    28.1 --- a/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 15:23:50 2015 +0200
    28.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 23:24:45 2015 +0200
    28.3 @@ -266,7 +266,7 @@
    28.4  (* Isar command *)
    28.5  
    28.6  val _ =
    28.7 -  Outer_Syntax.command @{command_spec "boogie_file"}
    28.8 +  Outer_Syntax.command @{command_keyword boogie_file}
    28.9      "prove verification condition from .b2i file"
   28.10      (Resources.provide_parse_files "boogie_file" >> (fn files =>
   28.11        Toplevel.theory (fn thy =>
    29.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 15:23:50 2015 +0200
    29.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 23:24:45 2015 +0200
    29.3 @@ -23,7 +23,9 @@
    29.4  \label{sec:spark-commands}
    29.5  This section describes the syntax and effect of each of the commands provided
    29.6  by HOL-\SPARK{}.
    29.7 -@{rail "@'spark_open' name ('(' name ')')?"}
    29.8 +@{rail \<open>
    29.9 +  @'spark_open' name ('(' name ')')?
   29.10 +\<close>}
   29.11  Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
   29.12  Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
   29.13  The corresponding \texttt{*.fdl} and \texttt{*.rls}
   29.14 @@ -36,7 +38,9 @@
   29.15  format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
   29.16  packages, this is necessary in order for the verification environment to be able to map proof
   29.17  functions and types defined in Isabelle to their \SPARK{} counterparts.
   29.18 -@{rail "@'spark_proof_functions' ((name '=' term)+)"}
   29.19 +@{rail \<open>
   29.20 +  @'spark_proof_functions' ((name '=' term)+)
   29.21 +\<close>}
   29.22  Associates a proof function with the given name to a term. The name should be the full name
   29.23  of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
   29.24  This command can be used both inside and outside a verification environment. The latter
   29.25 @@ -44,8 +48,11 @@
   29.26  or packages, whereas the former allows the given term to refer to the types generated
   29.27  by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
   29.28  \texttt{*.fdl} file.
   29.29 -@{rail "@'spark_types' ((name '=' type (mapping?))+);
   29.30 -mapping: '('((name '=' nameref)+',')')'"}
   29.31 +@{rail \<open>
   29.32 +  @'spark_types' ((name '=' type (mapping?))+)
   29.33 +  ;
   29.34 +  mapping: '('((name '=' nameref)+',')')'
   29.35 +\<close>}
   29.36  Associates a \SPARK{} type with the given name with an Isabelle type. This command can
   29.37  only be used outside a verification environment. The given type must be either a record
   29.38  or a datatype, where the names of fields or constructors must either match those of the
   29.39 @@ -57,18 +64,24 @@
   29.40  using Isabelle's commands for defining records or datatypes. Having introduced the
   29.41  types, the proof functions can be defined in Isabelle. Finally, both the proof
   29.42  functions and the types can be associated with their \SPARK{} counterparts.
   29.43 -@{rail "@'spark_status' (('(proved)' | '(unproved)')?)"}
   29.44 +@{rail \<open>
   29.45 +  @'spark_status' (('(proved)' | '(unproved)')?)
   29.46 +\<close>}
   29.47  Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
   29.48  the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
   29.49  The output can be restricted to the proved or unproved VCs by giving the corresponding
   29.50  option to the command.
   29.51 -@{rail "@'spark_vc' name"}
   29.52 +@{rail \<open>
   29.53 +  @'spark_vc' name
   29.54 +\<close>}
   29.55  Initiates the proof of the VC with the given name. Similar to the standard
   29.56  \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
   29.57  must be followed by a sequence of proof commands. The command introduces the
   29.58  hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
   29.59  \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
   29.60 -@{rail "@'spark_end' '(incomplete)'?"}
   29.61 +@{rail \<open>
   29.62 +  @'spark_end' '(incomplete)'?
   29.63 +\<close>}
   29.64  Closes the current verification environment. Unless the \texttt{incomplete}
   29.65  option is given, all VCs must have been proved,
   29.66  otherwise the command issues an error message. As a side effect, the command
    30.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 06 15:23:50 2015 +0200
    30.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 06 23:24:45 2015 +0200
    30.3 @@ -92,13 +92,13 @@
    30.4    end;
    30.5  
    30.6  val _ =
    30.7 -  Outer_Syntax.command @{command_spec "spark_open_vcg"}
    30.8 +  Outer_Syntax.command @{command_keyword spark_open_vcg}
    30.9      "open a new SPARK environment and load a SPARK-generated .vcg file"
   30.10      (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
   30.11        >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
   30.12  
   30.13  val _ =
   30.14 -  Outer_Syntax.command @{command_spec "spark_open"}
   30.15 +  Outer_Syntax.command @{command_keyword spark_open}
   30.16      "open a new SPARK environment and load a SPARK-generated .siv file"
   30.17      (Resources.provide_parse_files "spark_open" -- Parse.parname
   30.18        >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
   30.19 @@ -107,13 +107,13 @@
   30.20    (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
   30.21  
   30.22  val _ =
   30.23 -  Outer_Syntax.command @{command_spec "spark_proof_functions"}
   30.24 +  Outer_Syntax.command @{command_keyword spark_proof_functions}
   30.25      "associate SPARK proof functions with terms"
   30.26      (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
   30.27        (Toplevel.theory o fold add_proof_fun_cmd));
   30.28  
   30.29  val _ =
   30.30 -  Outer_Syntax.command @{command_spec "spark_types"}
   30.31 +  Outer_Syntax.command @{command_keyword spark_types}
   30.32      "associate SPARK types with types"
   30.33      (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
   30.34         Scan.optional (Args.parens (Parse.list1
   30.35 @@ -121,12 +121,12 @@
   30.36         (Toplevel.theory o fold add_spark_type_cmd));
   30.37  
   30.38  val _ =
   30.39 -  Outer_Syntax.local_theory_to_proof @{command_spec "spark_vc"}
   30.40 +  Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
   30.41      "enter into proof mode for a specific verification condition"
   30.42      (Parse.name >> prove_vc);
   30.43  
   30.44  val _ =
   30.45 -  Outer_Syntax.command @{command_spec "spark_status"}
   30.46 +  Outer_Syntax.command @{command_keyword spark_status}
   30.47      "show the name and state of all loaded verification conditions"
   30.48      (Scan.optional
   30.49         (Args.parens
   30.50 @@ -136,7 +136,7 @@
   30.51          Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
   30.52  
   30.53  val _ =
   30.54 -  Outer_Syntax.command @{command_spec "spark_end"}
   30.55 +  Outer_Syntax.command @{command_keyword spark_end}
   30.56      "close the current SPARK environment"
   30.57      (Scan.optional (@{keyword "("} |-- Parse.!!!
   30.58           (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
    31.1 --- a/src/HOL/Statespace/state_space.ML	Mon Apr 06 15:23:50 2015 +0200
    31.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Apr 06 23:24:45 2015 +0200
    31.3 @@ -650,7 +650,7 @@
    31.4          (plus1_unless comp parent --
    31.5            Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
    31.6  val _ =
    31.7 -  Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
    31.8 +  Outer_Syntax.command @{command_keyword statespace} "define state-space as locale context"
    31.9      (statespace_decl >> (fn ((args, name), (parents, comps)) =>
   31.10        Toplevel.theory (define_statespace args name parents comps)));
   31.11  
    32.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 06 15:23:50 2015 +0200
    32.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 06 23:24:45 2015 +0200
    32.3 @@ -912,7 +912,7 @@
    32.4    in TPTP_Data.map (cons ((prob_name, result))) thy' end
    32.5  
    32.6  val _ =
    32.7 -  Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
    32.8 +  Outer_Syntax.command @{command_keyword import_tptp} "import TPTP problem"
    32.9      (Parse.path >> (fn name =>
   32.10        Toplevel.theory (fn thy =>
   32.11          let val path = Path.explode name
    33.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Apr 06 15:23:50 2015 +0200
    33.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Apr 06 23:24:45 2015 +0200
    33.3 @@ -1854,7 +1854,7 @@
    33.4  
    33.5  (*This has been disabled since it requires a hook to be specified to use "import_thm"
    33.6  val _ =
    33.7 -  Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
    33.8 +  Outer_Syntax.command @{command_keyword import_leo2_proof} "import TPTP proof"
    33.9      (Parse.path >> (fn name =>
   33.10        Toplevel.theory (fn thy =>
   33.11         let val path = Path.explode name
    34.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 06 15:23:50 2015 +0200
    34.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 06 23:24:45 2015 +0200
    34.3 @@ -1615,12 +1615,12 @@
    34.4    end;
    34.5  
    34.6  val _ =
    34.7 -  Outer_Syntax.command @{command_spec "print_bnfs"}
    34.8 +  Outer_Syntax.command @{command_keyword print_bnfs}
    34.9      "print all bounded natural functors"
   34.10      (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
   34.11  
   34.12  val _ =
   34.13 -  Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
   34.14 +  Outer_Syntax.local_theory_to_proof @{command_keyword bnf}
   34.15      "register a type as a bounded natural functor"
   34.16      (parse_opt_binding_colon -- Parse.typ --|
   34.17         (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
    35.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 06 15:23:50 2015 +0200
    35.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 06 23:24:45 2015 +0200
    35.3 @@ -2019,7 +2019,7 @@
    35.4              val fake_T = qsoty (unfreeze_fp X);
    35.5              val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
    35.6              fun register_hint () =
    35.7 -              "\nUse the " ^ quote (#1 @{command_spec "bnf"}) ^ " command to register " ^
    35.8 +              "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
    35.9                quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
   35.10                \it";
   35.11            in
    36.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 15:23:50 2015 +0200
    36.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 23:24:45 2015 +0200
    36.3 @@ -2555,7 +2555,7 @@
    36.4    end;
    36.5  
    36.6  val _ =
    36.7 -  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
    36.8 +  Outer_Syntax.local_theory @{command_keyword codatatype} "define coinductive datatypes"
    36.9      (parse_co_datatype_cmd Greatest_FP construct_gfp);
   36.10  
   36.11  val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
    37.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 15:23:50 2015 +0200
    37.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 23:24:45 2015 +0200
    37.3 @@ -112,8 +112,8 @@
    37.4  fun unexpected_corec_call ctxt eqns t =
    37.5    error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
    37.6  fun use_primcorecursive () =
    37.7 -  error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
    37.8 -    quote (#1 @{command_spec "primcorec"}) ^ ")");
    37.9 +  error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
   37.10 +    quote (#1 @{command_keyword primcorec}) ^ ")");
   37.11  
   37.12  datatype corec_option =
   37.13    Plugins_Option of Proof.context -> Plugin_Name.filter |
   37.14 @@ -1551,13 +1551,13 @@
   37.15  val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
   37.16    ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
   37.17  
   37.18 -val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
   37.19 +val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
   37.20    "define primitive corecursive functions"
   37.21    ((Scan.optional (@{keyword "("} |--
   37.22        Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
   37.23      (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
   37.24  
   37.25 -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
   37.26 +val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   37.27    "define primitive corecursive functions"
   37.28    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
   37.29        --| @{keyword ")"}) []) --
    38.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 06 15:23:50 2015 +0200
    38.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 06 23:24:45 2015 +0200
    38.3 @@ -1842,7 +1842,7 @@
    38.4    end;
    38.5  
    38.6  val _ =
    38.7 -  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
    38.8 +  Outer_Syntax.local_theory @{command_keyword datatype} "define inductive datatypes"
    38.9      (parse_co_datatype_cmd Least_FP construct_lfp);
   38.10  
   38.11  val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
    39.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Apr 06 15:23:50 2015 +0200
    39.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Apr 06 23:24:45 2015 +0200
    39.3 @@ -539,7 +539,7 @@
    39.4    BNF_LFP_Rec_Sugar.add_primrec_simple;
    39.5  
    39.6  val _ =
    39.7 -  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
    39.8 +  Outer_Syntax.local_theory @{command_keyword datatype_compat}
    39.9      "register datatypes as old-style datatypes and derive old-style properties"
   39.10      (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
   39.11  
    40.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Apr 06 15:23:50 2015 +0200
    40.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Apr 06 23:24:45 2015 +0200
    40.3 @@ -669,7 +669,7 @@
    40.4     || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
    40.5     || Parse.reserved "transfer" >> K Transfer_Option);
    40.6  
    40.7 -val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
    40.8 +val _ = Outer_Syntax.local_theory @{command_keyword primrec}
    40.9    "define primitive recursive functions"
   40.10    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
   40.11        --| @{keyword ")"}) []) --
    41.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Apr 06 15:23:50 2015 +0200
    41.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Apr 06 23:24:45 2015 +0200
    41.3 @@ -630,7 +630,7 @@
    41.4    end;
    41.5  
    41.6  val _ =
    41.7 -  Outer_Syntax.command @{command_spec "print_case_translations"}
    41.8 +  Outer_Syntax.command @{command_keyword print_case_translations}
    41.9      "print registered case combinators and constructors"
   41.10      (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
   41.11  
    42.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 06 15:23:50 2015 +0200
    42.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 06 23:24:45 2015 +0200
    42.3 @@ -1143,7 +1143,7 @@
    42.4  val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
    42.5  
    42.6  val _ =
    42.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    42.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword free_constructors}
    42.9      "register an existing freely generated type's constructors"
   42.10      (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
   42.11         -- parse_sel_default_eqs
    43.1 --- a/src/HOL/Tools/Function/fun.ML	Mon Apr 06 15:23:50 2015 +0200
    43.2 +++ b/src/HOL/Tools/Function/fun.ML	Mon Apr 06 23:24:45 2015 +0200
    43.3 @@ -172,7 +172,7 @@
    43.4  
    43.5  
    43.6  val _ =
    43.7 -  Outer_Syntax.local_theory' @{command_spec "fun"}
    43.8 +  Outer_Syntax.local_theory' @{command_keyword fun}
    43.9      "define general recursive functions (short version)"
   43.10      (function_parser fun_config
   43.11        >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
    44.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 15:23:50 2015 +0200
    44.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 23:24:45 2015 +0200
    44.3 @@ -54,7 +54,7 @@
    44.4  val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
    44.5  
    44.6  val _ =
    44.7 -  Outer_Syntax.local_theory @{command_spec "fun_cases"}
    44.8 +  Outer_Syntax.local_theory @{command_keyword fun_cases}
    44.9      "create simplified instances of elimination rules for function equations"
   44.10      (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
   44.11  
    45.1 --- a/src/HOL/Tools/Function/function.ML	Mon Apr 06 15:23:50 2015 +0200
    45.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Apr 06 23:24:45 2015 +0200
    45.3 @@ -286,13 +286,13 @@
    45.4  (* outer syntax *)
    45.5  
    45.6  val _ =
    45.7 -  Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
    45.8 +  Outer_Syntax.local_theory_to_proof' @{command_keyword function}
    45.9      "define general recursive functions"
   45.10      (function_parser default_config
   45.11        >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
   45.12  
   45.13  val _ =
   45.14 -  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
   45.15 +  Outer_Syntax.local_theory_to_proof @{command_keyword termination}
   45.16      "prove termination of a recursive function"
   45.17      (Scan.option Parse.term >> termination_cmd)
   45.18  
    46.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 15:23:50 2015 +0200
    46.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 23:24:45 2015 +0200
    46.3 @@ -309,7 +309,7 @@
    46.4  val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
    46.5  
    46.6  val _ =
    46.7 -  Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
    46.8 +  Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
    46.9      ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
   46.10        >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
   46.11  
    47.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 06 15:23:50 2015 +0200
    47.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 06 23:24:45 2015 +0200
    47.3 @@ -700,7 +700,7 @@
    47.4      --| @{keyword "is"} -- Parse.term -- 
    47.5        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
    47.6  val _ =
    47.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
    47.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
    47.9      "definition for constants over the quotient type"
   47.10        (liftdef_parser >> lift_def_cmd_with_err_handling)
   47.11  
    48.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Apr 06 15:23:50 2015 +0200
    48.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Apr 06 23:24:45 2015 +0200
    48.3 @@ -533,11 +533,11 @@
    48.4  (* outer syntax commands *)
    48.5  
    48.6  val _ =
    48.7 -  Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
    48.8 +  Outer_Syntax.command @{command_keyword print_quot_maps} "print quotient map functions"
    48.9      (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
   48.10  
   48.11  val _ =
   48.12 -  Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
   48.13 +  Outer_Syntax.command @{command_keyword print_quotients} "print quotients"
   48.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   48.15  
   48.16  end
    49.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 06 15:23:50 2015 +0200
    49.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 06 23:24:45 2015 +0200
    49.3 @@ -787,7 +787,7 @@
    49.4    end
    49.5  
    49.6  val _ = 
    49.7 -  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
    49.8 +  Outer_Syntax.local_theory @{command_keyword setup_lifting}
    49.9      "setup lifting infrastructure" 
   49.10        (Parse.xthm -- Scan.option Parse.xthm 
   49.11        -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
   49.12 @@ -998,7 +998,7 @@
   49.13  
   49.14  
   49.15  val _ =
   49.16 -  Outer_Syntax.local_theory @{command_spec "lifting_forget"} 
   49.17 +  Outer_Syntax.local_theory @{command_keyword lifting_forget} 
   49.18      "unsetup Lifting and Transfer for the given lifting bundle"
   49.19      (Parse.position Parse.xname >> (lifting_forget_cmd))
   49.20  
   49.21 @@ -1027,7 +1027,7 @@
   49.22    update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
   49.23  
   49.24  val _ =
   49.25 -  Outer_Syntax.local_theory @{command_spec "lifting_update"}
   49.26 +  Outer_Syntax.local_theory @{command_keyword lifting_update}
   49.27      "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
   49.28      (Parse.position Parse.xname >> lifting_update_cmd)
   49.29  
    50.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 15:23:50 2015 +0200
    50.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 23:24:45 2015 +0200
    50.3 @@ -374,7 +374,7 @@
    50.4                                        |> sort_strings |> cat_lines)))))
    50.5  
    50.6  val _ =
    50.7 -  Outer_Syntax.command @{command_spec "nitpick"}
    50.8 +  Outer_Syntax.command @{command_keyword nitpick}
    50.9      "try to find a counterexample for a given subgoal using Nitpick"
   50.10      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   50.11        Toplevel.unknown_proof o
   50.12 @@ -383,7 +383,7 @@
   50.13            (Toplevel.proof_of state)))))
   50.14  
   50.15  val _ =
   50.16 -  Outer_Syntax.command @{command_spec "nitpick_params"}
   50.17 +  Outer_Syntax.command @{command_keyword nitpick_params}
   50.18      "set and display the default parameters for Nitpick"
   50.19      (parse_params #>> nitpick_params_trans)
   50.20  
    51.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Apr 06 15:23:50 2015 +0200
    51.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Apr 06 23:24:45 2015 +0200
    51.3 @@ -788,7 +788,7 @@
    51.4    >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
    51.5  
    51.6  val _ =
    51.7 -  Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
    51.8 +  Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
    51.9      (Parse.and_list1 spec_cmd
   51.10        >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
   51.11  
    52.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Apr 06 15:23:50 2015 +0200
    52.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Apr 06 23:24:45 2015 +0200
    52.3 @@ -680,7 +680,7 @@
    52.4  (* outer syntax *)
    52.5  
    52.6  val _ =
    52.7 -  Outer_Syntax.command @{command_spec "old_rep_datatype"}
    52.8 +  Outer_Syntax.command @{command_keyword old_rep_datatype}
    52.9      "register existing types as old-style datatypes"
   52.10      (Scan.repeat1 Parse.term >> (fn ts =>
   52.11        Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));
    53.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Apr 06 15:23:50 2015 +0200
    53.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Apr 06 23:24:45 2015 +0200
    53.3 @@ -1033,7 +1033,7 @@
    53.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    53.5  
    53.6  val _ =
    53.7 -  Outer_Syntax.command @{command_spec "values_prolog"}
    53.8 +  Outer_Syntax.command @{command_keyword values_prolog}
    53.9      "enumerate and print comprehensions"
   53.10      (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
   53.11       >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
    54.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Apr 06 15:23:50 2015 +0200
    54.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Apr 06 23:24:45 2015 +0200
    54.3 @@ -278,12 +278,12 @@
    54.4  (* code_pred command and values command *)
    54.5  
    54.6  val _ =
    54.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
    54.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword code_pred}
    54.9      "prove equations for predicate specified by intro/elim rules"
   54.10      (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
   54.11  
   54.12  val _ =
   54.13 -  Outer_Syntax.command @{command_spec "values"}
   54.14 +  Outer_Syntax.command @{command_keyword values}
   54.15      "enumerate and print comprehensions"
   54.16      (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
   54.17        >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
    55.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Mon Apr 06 15:23:50 2015 +0200
    55.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Mon Apr 06 23:24:45 2015 +0200
    55.3 @@ -67,7 +67,7 @@
    55.4      Syntax.read_term
    55.5    
    55.6  val _ =
    55.7 -  Outer_Syntax.command @{command_spec "quickcheck_generator"}
    55.8 +  Outer_Syntax.command @{command_keyword quickcheck_generator}
    55.9      "define quickcheck generators for abstract types"
   55.10      ((Parse.type_const --
   55.11        Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
    56.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Apr 06 15:23:50 2015 +0200
    56.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Apr 06 23:24:45 2015 +0200
    56.3 @@ -111,7 +111,7 @@
    56.4  end
    56.5  
    56.6  val _ =
    56.7 -  Outer_Syntax.command @{command_spec "find_unused_assms"}
    56.8 +  Outer_Syntax.command @{command_keyword find_unused_assms}
    56.9      "find theorems with (potentially) superfluous assumptions"
   56.10      (Scan.option Parse.name >> (fn name =>
   56.11        Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
    57.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 06 15:23:50 2015 +0200
    57.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 06 23:24:45 2015 +0200
    57.3 @@ -213,7 +213,7 @@
    57.4      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
    57.5  
    57.6  val _ =
    57.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
    57.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition}
    57.9      "definition for constants over the quotient type"
   57.10        (quotdef_parser >> quotient_def_cmd)
   57.11  
    58.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Apr 06 15:23:50 2015 +0200
    58.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Apr 06 23:24:45 2015 +0200
    58.3 @@ -229,15 +229,15 @@
    58.4  (* outer syntax commands *)
    58.5  
    58.6  val _ =
    58.7 -  Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
    58.8 +  Outer_Syntax.command @{command_keyword print_quotmapsQ3} "print quotient map functions"
    58.9      (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   58.10  
   58.11  val _ =
   58.12 -  Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
   58.13 +  Outer_Syntax.command @{command_keyword print_quotientsQ3} "print quotients"
   58.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   58.15  
   58.16  val _ =
   58.17 -  Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
   58.18 +  Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
   58.19      (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   58.20  
   58.21  end;
    59.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 06 15:23:50 2015 +0200
    59.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 06 23:24:45 2015 +0200
    59.3 @@ -342,7 +342,7 @@
    59.4            -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
    59.5  
    59.6  val _ =
    59.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
    59.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
    59.9      "quotient type definitions (require equivalence proofs)"
   59.10        (quotspec_parser >> quotient_type_cmd)
   59.11  
    60.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Apr 06 15:23:50 2015 +0200
    60.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Apr 06 23:24:45 2015 +0200
    60.3 @@ -257,7 +257,7 @@
    60.4    end
    60.5  
    60.6  val _ =
    60.7 -  Outer_Syntax.command @{command_spec "smt_status"}
    60.8 +  Outer_Syntax.command @{command_keyword smt_status}
    60.9      "show the available SMT solvers, the currently selected SMT solver, \
   60.10      \and the values of SMT configuration options"
   60.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    61.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 06 15:23:50 2015 +0200
    61.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 06 23:24:45 2015 +0200
    61.3 @@ -387,12 +387,12 @@
    61.4      no_fact_override
    61.5  
    61.6  val _ =
    61.7 -  Outer_Syntax.command @{command_spec "sledgehammer"}
    61.8 +  Outer_Syntax.command @{command_keyword sledgehammer}
    61.9      "search for first-order proof using automatic theorem provers"
   61.10      ((Scan.optional Parse.name runN -- parse_params
   61.11        -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
   61.12  val _ =
   61.13 -  Outer_Syntax.command @{command_spec "sledgehammer_params"}
   61.14 +  Outer_Syntax.command @{command_keyword sledgehammer_params}
   61.15      "set and display the default parameters for Sledgehammer"
   61.16      (parse_params #>> sledgehammer_params_trans)
   61.17  
    62.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Apr 06 15:23:50 2015 +0200
    62.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Apr 06 23:24:45 2015 +0200
    62.3 @@ -198,7 +198,7 @@
    62.4  val opt_overloaded = Parse.opt_keyword "overloaded"
    62.5  
    62.6  val _ =
    62.7 -  Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
    62.8 +  Outer_Syntax.command @{command_keyword specification} "define constants by specification"
    62.9      (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
   62.10        Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
   62.11        >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
    63.1 --- a/src/HOL/Tools/functor.ML	Mon Apr 06 15:23:50 2015 +0200
    63.2 +++ b/src/HOL/Tools/functor.ML	Mon Apr 06 23:24:45 2015 +0200
    63.3 @@ -273,7 +273,7 @@
    63.4  val functor_cmd = gen_functor Syntax.read_term;
    63.5  
    63.6  val _ =
    63.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
    63.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword functor}
    63.9      "register operations managing the functorial structure of a type"
   63.10      (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
   63.11        >> (fn (prfx, t) => functor_cmd prfx t));
    64.1 --- a/src/HOL/Tools/inductive.ML	Mon Apr 06 15:23:50 2015 +0200
    64.2 +++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 23:24:45 2015 +0200
    64.3 @@ -97,9 +97,8 @@
    64.4  
    64.5  (** theory context references **)
    64.6  
    64.7 -val inductive_forall_def = @{thm induct_forall_def};
    64.8 -val inductive_conj_name = "HOL.induct_conj";
    64.9 -val inductive_conj_def = @{thm induct_conj_def};
   64.10 +val inductive_forall_def = @{thm HOL.induct_forall_def};
   64.11 +val inductive_conj_def = @{thm HOL.induct_conj_def};
   64.12  val inductive_conj = @{thms induct_conj};
   64.13  val inductive_atomize = @{thms induct_atomize};
   64.14  val inductive_rulify = @{thms induct_rulify};
   64.15 @@ -689,7 +688,7 @@
   64.16                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
   64.17                  val Q =
   64.18                    fold_rev Term.abs (mk_names "x" k ~~ Ts)
   64.19 -                    (HOLogic.mk_binop inductive_conj_name
   64.20 +                    (HOLogic.mk_binop @{const_name HOL.induct_conj}
   64.21                        (list_comb (incr_boundvars k s, bs), P));
   64.22                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
   64.23            | NONE =>
   64.24 @@ -1171,25 +1170,25 @@
   64.25  val ind_decl = gen_ind_decl add_ind_def;
   64.26  
   64.27  val _ =
   64.28 -  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
   64.29 +  Outer_Syntax.local_theory @{command_keyword inductive} "define inductive predicates"
   64.30      (ind_decl false);
   64.31  
   64.32  val _ =
   64.33 -  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
   64.34 +  Outer_Syntax.local_theory @{command_keyword coinductive} "define coinductive predicates"
   64.35      (ind_decl true);
   64.36  
   64.37  val _ =
   64.38 -  Outer_Syntax.local_theory @{command_spec "inductive_cases"}
   64.39 +  Outer_Syntax.local_theory @{command_keyword inductive_cases}
   64.40      "create simplified instances of elimination rules"
   64.41      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   64.42  
   64.43  val _ =
   64.44 -  Outer_Syntax.local_theory @{command_spec "inductive_simps"}
   64.45 +  Outer_Syntax.local_theory @{command_keyword inductive_simps}
   64.46      "create simplification rules for inductive predicates"
   64.47      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
   64.48  
   64.49  val _ =
   64.50 -  Outer_Syntax.command @{command_spec "print_inductives"}
   64.51 +  Outer_Syntax.command @{command_keyword print_inductives}
   64.52      "print (co)inductive definitions and monotonicity rules"
   64.53      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   64.54        Toplevel.keep (print_inductives b o Toplevel.context_of)));
    65.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Apr 06 15:23:50 2015 +0200
    65.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Apr 06 23:24:45 2015 +0200
    65.3 @@ -568,11 +568,11 @@
    65.4  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
    65.5  
    65.6  val _ =
    65.7 -  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
    65.8 +  Outer_Syntax.local_theory @{command_keyword inductive_set} "define inductive sets"
    65.9      (ind_set_decl false);
   65.10  
   65.11  val _ =
   65.12 -  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
   65.13 +  Outer_Syntax.local_theory @{command_keyword coinductive_set} "define coinductive sets"
   65.14      (ind_set_decl true);
   65.15  
   65.16  end;
    66.1 --- a/src/HOL/Tools/recdef.ML	Mon Apr 06 15:23:50 2015 +0200
    66.2 +++ b/src/HOL/Tools/recdef.ML	Mon Apr 06 23:24:45 2015 +0200
    66.3 @@ -298,7 +298,7 @@
    66.4    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
    66.5  
    66.6  val _ =
    66.7 -  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
    66.8 +  Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
    66.9      (recdef_decl >> Toplevel.theory);
   66.10  
   66.11  
   66.12 @@ -309,12 +309,12 @@
   66.13    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   66.14  
   66.15  val _ =
   66.16 -  Outer_Syntax.command @{command_spec "defer_recdef"}
   66.17 +  Outer_Syntax.command @{command_keyword defer_recdef}
   66.18      "defer general recursive functions (obsolete TFL)"
   66.19      (defer_recdef_decl >> Toplevel.theory);
   66.20  
   66.21  val _ =
   66.22 -  Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
   66.23 +  Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
   66.24      "recommence proof of termination condition (obsolete TFL)"
   66.25      ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   66.26          Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
    67.1 --- a/src/HOL/Tools/record.ML	Mon Apr 06 15:23:50 2015 +0200
    67.2 +++ b/src/HOL/Tools/record.ML	Mon Apr 06 23:24:45 2015 +0200
    67.3 @@ -2329,7 +2329,7 @@
    67.4  (* outer syntax *)
    67.5  
    67.6  val _ =
    67.7 -  Outer_Syntax.command @{command_spec "record"} "define extensible record"
    67.8 +  Outer_Syntax.command @{command_keyword record} "define extensible record"
    67.9      (Parse.type_args_constrained -- Parse.binding --
   67.10        (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
   67.11          Scan.repeat1 Parse.const_binding)
    68.1 --- a/src/HOL/Tools/try0.ML	Mon Apr 06 15:23:50 2015 +0200
    68.2 +++ b/src/HOL/Tools/try0.ML	Mon Apr 06 23:24:45 2015 +0200
    68.3 @@ -177,7 +177,7 @@
    68.4     || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
    68.5  
    68.6  val _ =
    68.7 -  Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
    68.8 +  Outer_Syntax.command @{command_keyword try0} "try a combination of proof methods"
    68.9      (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
   68.10  
   68.11  fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
    69.1 --- a/src/HOL/Tools/typedef.ML	Mon Apr 06 15:23:50 2015 +0200
    69.2 +++ b/src/HOL/Tools/typedef.ML	Mon Apr 06 23:24:45 2015 +0200
    69.3 @@ -281,7 +281,7 @@
    69.4  (** outer syntax **)
    69.5  
    69.6  val _ =
    69.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
    69.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
    69.9      "HOL type definition (requires non-emptiness proof)"
   69.10      (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
   69.11        (@{keyword "="} |-- Parse.term) --
    70.1 --- a/src/HOL/Tools/value.ML	Mon Apr 06 15:23:50 2015 +0200
    70.2 +++ b/src/HOL/Tools/value.ML	Mon Apr 06 23:24:45 2015 +0200
    70.3 @@ -70,7 +70,7 @@
    70.4    Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    70.5    
    70.6  val _ =
    70.7 -  Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
    70.8 +  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    70.9      (opt_evaluator -- opt_modes -- Parse.term
   70.10        >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
   70.11  
    71.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Mon Apr 06 15:23:50 2015 +0200
    71.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Apr 06 23:24:45 2015 +0200
    71.3 @@ -40,7 +40,7 @@
    71.4  subsection \<open>Outer syntax: cartouche within command syntax\<close>
    71.5  
    71.6  ML \<open>
    71.7 -  Outer_Syntax.command @{command_spec "cartouche"} ""
    71.8 +  Outer_Syntax.command @{command_keyword cartouche} ""
    71.9      (Parse.cartouche >> (fn s =>
   71.10        Toplevel.imperative (fn () => writeln s)))
   71.11  \<close>
   71.12 @@ -116,7 +116,7 @@
   71.13  subsubsection \<open>Term cartouche and regular quotes\<close>
   71.14  
   71.15  ML \<open>
   71.16 -  Outer_Syntax.command @{command_spec "term_cartouche"} ""
   71.17 +  Outer_Syntax.command @{command_keyword term_cartouche} ""
   71.18      (Parse.inner_syntax Parse.cartouche >> (fn s =>
   71.19        Toplevel.keep (fn state =>
   71.20          let
   71.21 @@ -178,7 +178,7 @@
   71.22  
   71.23  ML \<open>
   71.24    Outer_Syntax.command
   71.25 -    @{command_spec "text_cartouche"} ""
   71.26 +    @{command_keyword text_cartouche} ""
   71.27      (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
   71.28  \<close>
   71.29  
    72.1 --- a/src/HOL/ex/Commands.thy	Mon Apr 06 15:23:50 2015 +0200
    72.2 +++ b/src/HOL/ex/Commands.thy	Mon Apr 06 23:24:45 2015 +0200
    72.3 @@ -15,7 +15,7 @@
    72.4  subsection \<open>Diagnostic command: no state change\<close>
    72.5  
    72.6  ML \<open>
    72.7 -  Outer_Syntax.command @{command_spec "print_test"} "print term test"
    72.8 +  Outer_Syntax.command @{command_keyword print_test} "print term test"
    72.9      (Parse.term >> (fn s => Toplevel.keep (fn st =>
   72.10        let
   72.11          val ctxt = Toplevel.context_of st;
   72.12 @@ -30,7 +30,7 @@
   72.13  subsection \<open>Old-style global theory declaration\<close>
   72.14  
   72.15  ML \<open>
   72.16 -  Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
   72.17 +  Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
   72.18      (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
   72.19        let
   72.20          val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
   72.21 @@ -45,7 +45,7 @@
   72.22  subsection \<open>Local theory specification\<close>
   72.23  
   72.24  ML \<open>
   72.25 -  Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
   72.26 +  Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
   72.27      (Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
   72.28        let
   72.29          val t = Syntax.read_term lthy s;
    73.1 --- a/src/Provers/classical.ML	Mon Apr 06 15:23:50 2015 +0200
    73.2 +++ b/src/Provers/classical.ML	Mon Apr 06 23:24:45 2015 +0200
    73.3 @@ -974,7 +974,7 @@
    73.4  (** outer syntax **)
    73.5  
    73.6  val _ =
    73.7 -  Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
    73.8 +  Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
    73.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
   73.10  
   73.11  end;
    74.1 --- a/src/Pure/General/binding.ML	Mon Apr 06 15:23:50 2015 +0200
    74.2 +++ b/src/Pure/General/binding.ML	Mon Apr 06 23:24:45 2015 +0200
    74.3 @@ -31,7 +31,8 @@
    74.4    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    74.5    val prefix: bool -> string -> binding -> binding
    74.6    val private: scope -> binding -> binding
    74.7 -  val private_default: scope option -> binding -> binding
    74.8 +  val restricted: scope -> binding -> binding
    74.9 +  val limited_default: (bool * scope) option -> binding -> binding
   74.10    val concealed: binding -> binding
   74.11    val pretty: binding -> Pretty.T
   74.12    val print: binding -> string
   74.13 @@ -39,7 +40,7 @@
   74.14    val bad: binding -> string
   74.15    val check: binding -> unit
   74.16    val name_spec: scope list -> (string * bool) list -> binding ->
   74.17 -    {accessible: bool, concealed: bool, spec: (string * bool) list}
   74.18 +    {limitation: bool option, concealed: bool, spec: (string * bool) list}
   74.19  end;
   74.20  
   74.21  structure Binding: BINDING =
   74.22 @@ -47,7 +48,7 @@
   74.23  
   74.24  (** representation **)
   74.25  
   74.26 -(* scope of private entries *)
   74.27 +(* scope of limited entries *)
   74.28  
   74.29  datatype scope = Scope of serial;
   74.30  
   74.31 @@ -57,19 +58,19 @@
   74.32  (* binding *)
   74.33  
   74.34  datatype binding = Binding of
   74.35 - {private: scope option,            (*entry is strictly private within its scope*)
   74.36 -  concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   74.37 -  prefix: (string * bool) list,     (*system prefix*)
   74.38 -  qualifier: (string * bool) list,  (*user qualifier*)
   74.39 -  name: bstring,                    (*base name*)
   74.40 -  pos: Position.T};                 (*source position*)
   74.41 + {limited: (bool * scope) option,  (*entry is private (true) / restricted (false) to scope*)
   74.42 +  concealed: bool,                 (*entry is for foundational purposes -- please ignore*)
   74.43 +  prefix: (string * bool) list,    (*system prefix*)
   74.44 +  qualifier: (string * bool) list, (*user qualifier*)
   74.45 +  name: bstring,                   (*base name*)
   74.46 +  pos: Position.T};                (*source position*)
   74.47  
   74.48 -fun make_binding (private, concealed, prefix, qualifier, name, pos) =
   74.49 -  Binding {private = private, concealed = concealed, prefix = prefix,
   74.50 +fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
   74.51 +  Binding {limited = limited, concealed = concealed, prefix = prefix,
   74.52      qualifier = qualifier, name = name, pos = pos};
   74.53  
   74.54 -fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
   74.55 -  make_binding (f (private, concealed, prefix, qualifier, name, pos));
   74.56 +fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
   74.57 +  make_binding (f (limited, concealed, prefix, qualifier, name, pos));
   74.58  
   74.59  fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
   74.60  
   74.61 @@ -83,8 +84,8 @@
   74.62  
   74.63  fun pos_of (Binding {pos, ...}) = pos;
   74.64  fun set_pos pos =
   74.65 -  map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
   74.66 -    (private, concealed, prefix, qualifier, name, pos));
   74.67 +  map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
   74.68 +    (limited, concealed, prefix, qualifier, name, pos));
   74.69  
   74.70  fun name name = make (name, Position.none);
   74.71  fun name_of (Binding {name, ...}) = name;
   74.72 @@ -92,8 +93,8 @@
   74.73  fun eq_name (b, b') = name_of b = name_of b';
   74.74  
   74.75  fun map_name f =
   74.76 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   74.77 -    (private, concealed, prefix, qualifier, f name, pos));
   74.78 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   74.79 +    (limited, concealed, prefix, qualifier, f name, pos));
   74.80  
   74.81  val prefix_name = map_name o prefix;
   74.82  val suffix_name = map_name o suffix;
   74.83 @@ -106,13 +107,13 @@
   74.84  
   74.85  fun qualify _ "" = I
   74.86    | qualify mandatory qual =
   74.87 -      map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   74.88 -        (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
   74.89 +      map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   74.90 +        (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
   74.91  
   74.92  fun qualified mandatory name' =
   74.93 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   74.94 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   74.95      let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
   74.96 -    in (private, concealed, prefix, qualifier', name', pos) end);
   74.97 +    in (limited, concealed, prefix, qualifier', name', pos) end);
   74.98  
   74.99  fun qualified_name "" = empty
  74.100    | qualified_name s =
  74.101 @@ -125,8 +126,8 @@
  74.102  fun prefix_of (Binding {prefix, ...}) = prefix;
  74.103  
  74.104  fun map_prefix f =
  74.105 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
  74.106 -    (private, concealed, f prefix, qualifier, name, pos));
  74.107 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
  74.108 +    (limited, concealed, f prefix, qualifier, name, pos));
  74.109  
  74.110  fun prefix _ "" = I
  74.111    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
  74.112 @@ -134,17 +135,20 @@
  74.113  
  74.114  (* visibility flags *)
  74.115  
  74.116 -fun private scope =
  74.117 +fun limited strict scope =
  74.118    map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
  74.119 -    (SOME scope, concealed, prefix, qualifier, name, pos));
  74.120 +    (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
  74.121  
  74.122 -fun private_default private' =
  74.123 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
  74.124 -    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
  74.125 +val private = limited true;
  74.126 +val restricted = limited false;
  74.127 +
  74.128 +fun limited_default limited' =
  74.129 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
  74.130 +    (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
  74.131  
  74.132  val concealed =
  74.133 -  map_binding (fn (private, _, prefix, qualifier, name, pos) =>
  74.134 -    (private, true, prefix, qualifier, name, pos));
  74.135 +  map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
  74.136 +    (limited, true, prefix, qualifier, name, pos));
  74.137  
  74.138  
  74.139  (* print *)
  74.140 @@ -177,13 +181,13 @@
  74.141  
  74.142  fun name_spec scopes path binding =
  74.143    let
  74.144 -    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
  74.145 +    val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
  74.146      val _ = Long_Name.is_qualified name andalso error (bad binding);
  74.147  
  74.148 -    val accessible =
  74.149 -      (case private of
  74.150 -        NONE => true
  74.151 -      | SOME scope => member (op =) scopes scope);
  74.152 +    val limitation =
  74.153 +      (case limited of
  74.154 +        NONE => NONE
  74.155 +      | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
  74.156  
  74.157      val spec1 =
  74.158        maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
  74.159 @@ -192,7 +196,7 @@
  74.160      val _ =
  74.161        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
  74.162        andalso error (bad binding);
  74.163 -  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
  74.164 +  in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
  74.165  
  74.166  end;
  74.167  
    75.1 --- a/src/Pure/General/name_space.ML	Mon Apr 06 15:23:50 2015 +0200
    75.2 +++ b/src/Pure/General/name_space.ML	Mon Apr 06 23:24:45 2015 +0200
    75.3 @@ -35,8 +35,11 @@
    75.4    val get_scopes: naming -> Binding.scope list
    75.5    val get_scope: naming -> Binding.scope option
    75.6    val new_scope: naming -> Binding.scope * naming
    75.7 +  val limited: bool -> Position.T -> naming -> naming
    75.8    val private_scope: Binding.scope -> naming -> naming
    75.9    val private: Position.T -> naming -> naming
   75.10 +  val restricted_scope: Binding.scope -> naming -> naming
   75.11 +  val restricted: Position.T -> naming -> naming
   75.12    val concealed: naming -> naming
   75.13    val get_group: naming -> serial option
   75.14    val set_group: serial option -> naming -> naming
   75.15 @@ -297,62 +300,73 @@
   75.16  
   75.17  datatype naming = Naming of
   75.18   {scopes: Binding.scope list,
   75.19 -  private: Binding.scope option,
   75.20 +  limited: (bool * Binding.scope) option,
   75.21    concealed: bool,
   75.22    group: serial option,
   75.23    theory_name: string,
   75.24    path: (string * bool) list};
   75.25  
   75.26 -fun make_naming (scopes, private, concealed, group, theory_name, path) =
   75.27 -  Naming {scopes = scopes, private = private, concealed = concealed,
   75.28 +fun make_naming (scopes, limited, concealed, group, theory_name, path) =
   75.29 +  Naming {scopes = scopes, limited = limited, concealed = concealed,
   75.30      group = group, theory_name = theory_name, path = path};
   75.31  
   75.32 -fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
   75.33 -  make_naming (f (scopes, private, concealed, group, theory_name, path));
   75.34 +fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
   75.35 +  make_naming (f (scopes, limited, concealed, group, theory_name, path));
   75.36  
   75.37 -fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
   75.38 -  (scopes, private, concealed, group, theory_name, f path));
   75.39  
   75.40 +(* scope and access limitation *)
   75.41  
   75.42  fun get_scopes (Naming {scopes, ...}) = scopes;
   75.43  val get_scope = try hd o get_scopes;
   75.44  
   75.45 -fun put_scope scope =
   75.46 -  map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
   75.47 -    (scope :: scopes, private, concealed, group, theory_name, path));
   75.48 -
   75.49  fun new_scope naming =
   75.50    let
   75.51      val scope = Binding.new_scope ();
   75.52      val naming' =
   75.53 -      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
   75.54 -        (scope :: scopes, private, concealed, group, theory_name, path));
   75.55 +      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
   75.56 +        (scope :: scopes, limited, concealed, group, theory_name, path));
   75.57    in (scope, naming') end;
   75.58  
   75.59 -fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
   75.60 -  (scopes, SOME scope, concealed, group, theory_name, path));
   75.61 +fun limited_scope strict scope =
   75.62 +  map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
   75.63 +    (scopes, SOME (strict, scope), concealed, group, theory_name, path));
   75.64  
   75.65 -fun private pos naming =
   75.66 +fun limited strict pos naming =
   75.67    (case get_scope naming of
   75.68 -    SOME scope => private_scope scope naming
   75.69 -  | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
   75.70 +    SOME scope => limited_scope strict scope naming
   75.71 +  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
   75.72 +
   75.73 +val private_scope = limited_scope true;
   75.74 +val private = limited true;
   75.75 +
   75.76 +val restricted_scope = limited_scope false;
   75.77 +val restricted = limited false;
   75.78  
   75.79 -val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
   75.80 -  (scopes, private, true, group, theory_name, path));
   75.81 +val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
   75.82 +  (scopes, limited, true, group, theory_name, path));
   75.83 +
   75.84  
   75.85 -fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
   75.86 -  (scopes, private, concealed, group, theory_name, path));
   75.87 +(* additional structural info *)
   75.88 +
   75.89 +fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
   75.90 +  (scopes, limited, concealed, group, theory_name, path));
   75.91  
   75.92  fun get_group (Naming {group, ...}) = group;
   75.93  
   75.94 -fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
   75.95 -  (scopes, private, concealed, group, theory_name, path));
   75.96 +fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
   75.97 +  (scopes, limited, concealed, group, theory_name, path));
   75.98  
   75.99  fun new_group naming = set_group (SOME (serial ())) naming;
  75.100  val reset_group = set_group NONE;
  75.101  
  75.102 +
  75.103 +(* name entry path *)
  75.104 +
  75.105  fun get_path (Naming {path, ...}) = path;
  75.106  
  75.107 +fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
  75.108 +  (scopes, limited, concealed, group, theory_name, f path));
  75.109 +
  75.110  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
  75.111  val root_path = map_path (fn _ => []);
  75.112  val parent_path = map_path (perhaps (try (#1 o split_last)));
  75.113 @@ -365,14 +379,16 @@
  75.114  val local_naming = global_naming |> add_path Long_Name.localN;
  75.115  
  75.116  
  75.117 -(* visibility flags *)
  75.118 +(* transform *)
  75.119  
  75.120 -fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
  75.121 -  fold private_scope (the_list private') #>
  75.122 +fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
  75.123 +  (case limited' of
  75.124 +    SOME (strict, scope) => limited_scope strict scope
  75.125 +  | NONE => I) #>
  75.126    concealed' ? concealed;
  75.127  
  75.128 -fun transform_binding (Naming {private, concealed, ...}) =
  75.129 -  Binding.private_default private #>
  75.130 +fun transform_binding (Naming {limited, concealed, ...}) =
  75.131 +  Binding.limited_default limited #>
  75.132    concealed ? Binding.concealed;
  75.133  
  75.134  
  75.135 @@ -400,11 +416,12 @@
  75.136  
  75.137  fun accesses naming binding =
  75.138    (case name_spec naming binding of
  75.139 -    {accessible = false, ...} => ([], [])
  75.140 -  | {spec, ...} =>
  75.141 +    {limitation = SOME true, ...} => ([], [])
  75.142 +  | {limitation, spec, ...} =>
  75.143        let
  75.144 -        val sfxs = mandatory_suffixes spec;
  75.145 -        val pfxs = mandatory_prefixes spec;
  75.146 +        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
  75.147 +        val sfxs = restrict (mandatory_suffixes spec);
  75.148 +        val pfxs = restrict (mandatory_prefixes spec);
  75.149        in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
  75.150  
  75.151  
    76.1 --- a/src/Pure/Isar/calculation.ML	Mon Apr 06 15:23:50 2015 +0200
    76.2 +++ b/src/Pure/Isar/calculation.ML	Mon Apr 06 23:24:45 2015 +0200
    76.3 @@ -211,25 +211,25 @@
    76.4    Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
    76.5  
    76.6  val _ =
    76.7 -  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
    76.8 +  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
    76.9      (calc_args >> (Toplevel.proofs' o also_cmd));
   76.10  
   76.11  val _ =
   76.12 -  Outer_Syntax.command @{command_spec "finally"}
   76.13 +  Outer_Syntax.command @{command_keyword finally}
   76.14      "combine calculation and current facts, exhibit result"
   76.15      (calc_args >> (Toplevel.proofs' o finally_cmd));
   76.16  
   76.17  val _ =
   76.18 -  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
   76.19 +  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
   76.20      (Scan.succeed (Toplevel.proof' moreover));
   76.21  
   76.22  val _ =
   76.23 -  Outer_Syntax.command @{command_spec "ultimately"}
   76.24 +  Outer_Syntax.command @{command_keyword ultimately}
   76.25      "augment calculation by current facts, exhibit result"
   76.26      (Scan.succeed (Toplevel.proof' ultimately));
   76.27  
   76.28  val _ =
   76.29 -  Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
   76.30 +  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   76.31      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
   76.32  
   76.33  end;
    77.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 15:23:50 2015 +0200
    77.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 23:24:45 2015 +0200
    77.3 @@ -6,7 +6,7 @@
    77.4  
    77.5  signature ISAR_CMD =
    77.6  sig
    77.7 -  val global_setup: Input.source -> theory -> theory
    77.8 +  val setup: Input.source -> theory -> theory
    77.9    val local_setup: Input.source -> Proof.context -> Proof.context
   77.10    val parse_ast_translation: Input.source -> theory -> theory
   77.11    val parse_translation: Input.source -> theory -> theory
   77.12 @@ -57,7 +57,7 @@
   77.13  
   77.14  (* generic setup *)
   77.15  
   77.16 -fun global_setup source =
   77.17 +fun setup source =
   77.18    ML_Lex.read_source false source
   77.19    |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
   77.20      "Context.map_theory setup"
    78.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 06 15:23:50 2015 +0200
    78.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 06 23:24:45 2015 +0200
    78.3 @@ -12,7 +12,7 @@
    78.4  (* sorts *)
    78.5  
    78.6  val _ =
    78.7 -  Outer_Syntax.local_theory @{command_spec "default_sort"}
    78.8 +  Outer_Syntax.local_theory @{command_keyword default_sort}
    78.9      "declare default sort for explicit type variables"
   78.10      (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   78.11  
   78.12 @@ -20,18 +20,18 @@
   78.13  (* types *)
   78.14  
   78.15  val _ =
   78.16 -  Outer_Syntax.local_theory @{command_spec "typedecl"} "type declaration"
   78.17 +  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
   78.18      (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   78.19        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
   78.20  
   78.21  val _ =
   78.22 -  Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
   78.23 +  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
   78.24      (Parse.type_args -- Parse.binding --
   78.25        (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
   78.26        >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   78.27  
   78.28  val _ =
   78.29 -  Outer_Syntax.command @{command_spec "nonterminal"}
   78.30 +  Outer_Syntax.command @{command_keyword nonterminal}
   78.31      "declare syntactic type constructors (grammar nonterminal symbols)"
   78.32      (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
   78.33  
   78.34 @@ -39,11 +39,11 @@
   78.35  (* consts and syntax *)
   78.36  
   78.37  val _ =
   78.38 -  Outer_Syntax.command @{command_spec "judgment"} "declare object-logic judgment"
   78.39 +  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
   78.40      (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   78.41  
   78.42  val _ =
   78.43 -  Outer_Syntax.command @{command_spec "consts"} "declare constants"
   78.44 +  Outer_Syntax.command @{command_keyword consts} "declare constants"
   78.45      (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
   78.46  
   78.47  val mode_spec =
   78.48 @@ -54,12 +54,12 @@
   78.49    Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
   78.50  
   78.51  val _ =
   78.52 -  Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
   78.53 +  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
   78.54      (opt_mode -- Scan.repeat1 Parse.const_decl
   78.55        >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   78.56  
   78.57  val _ =
   78.58 -  Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
   78.59 +  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
   78.60      (opt_mode -- Scan.repeat1 Parse.const_decl
   78.61        >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   78.62  
   78.63 @@ -81,11 +81,11 @@
   78.64      >> (fn (left, (arr, right)) => arr (left, right));
   78.65  
   78.66  val _ =
   78.67 -  Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
   78.68 +  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
   78.69      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   78.70  
   78.71  val _ =
   78.72 -  Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
   78.73 +  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
   78.74      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   78.75  
   78.76  
   78.77 @@ -98,7 +98,7 @@
   78.78        @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
   78.79  
   78.80  val _ =
   78.81 -  Outer_Syntax.command @{command_spec "defs"} "define constants"
   78.82 +  Outer_Syntax.command @{command_keyword defs} "define constants"
   78.83      (opt_unchecked_overloaded --
   78.84        Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
   78.85        >> (Toplevel.theory o Isar_Cmd.add_defs));
   78.86 @@ -107,34 +107,34 @@
   78.87  (* constant definitions and abbreviations *)
   78.88  
   78.89  val _ =
   78.90 -  Outer_Syntax.local_theory' @{command_spec "definition"} "constant definition"
   78.91 +  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
   78.92      (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
   78.93  
   78.94  val _ =
   78.95 -  Outer_Syntax.local_theory' @{command_spec "abbreviation"} "constant abbreviation"
   78.96 +  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   78.97      (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   78.98        >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   78.99  
  78.100  val _ =
  78.101 -  Outer_Syntax.local_theory @{command_spec "type_notation"}
  78.102 +  Outer_Syntax.local_theory @{command_keyword type_notation}
  78.103      "add concrete syntax for type constructors"
  78.104      (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  78.105        >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
  78.106  
  78.107  val _ =
  78.108 -  Outer_Syntax.local_theory @{command_spec "no_type_notation"}
  78.109 +  Outer_Syntax.local_theory @{command_keyword no_type_notation}
  78.110      "delete concrete syntax for type constructors"
  78.111      (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  78.112        >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
  78.113  
  78.114  val _ =
  78.115 -  Outer_Syntax.local_theory @{command_spec "notation"}
  78.116 +  Outer_Syntax.local_theory @{command_keyword notation}
  78.117      "add concrete syntax for constants / fixed variables"
  78.118      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  78.119        >> (fn (mode, args) => Specification.notation_cmd true mode args));
  78.120  
  78.121  val _ =
  78.122 -  Outer_Syntax.local_theory @{command_spec "no_notation"}
  78.123 +  Outer_Syntax.local_theory @{command_keyword no_notation}
  78.124      "delete concrete syntax for constants / fixed variables"
  78.125      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  78.126        >> (fn (mode, args) => Specification.notation_cmd false mode args));
  78.127 @@ -143,7 +143,7 @@
  78.128  (* constant specifications *)
  78.129  
  78.130  val _ =
  78.131 -  Outer_Syntax.command @{command_spec "axiomatization"} "axiomatic constant specification"
  78.132 +  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
  78.133      (Scan.optional Parse.fixes [] --
  78.134        Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
  78.135        >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
  78.136 @@ -156,14 +156,14 @@
  78.137      >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
  78.138  
  78.139  val _ =
  78.140 -  Outer_Syntax.local_theory' @{command_spec "theorems"} "define theorems"
  78.141 +  Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems"
  78.142      (theorems Thm.theoremK);
  78.143  
  78.144  val _ =
  78.145 -  Outer_Syntax.local_theory' @{command_spec "lemmas"} "define lemmas" (theorems Thm.lemmaK);
  78.146 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" (theorems Thm.lemmaK);
  78.147  
  78.148  val _ =
  78.149 -  Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
  78.150 +  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
  78.151      (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
  78.152        >> (fn (facts, fixes) =>
  78.153            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
  78.154 @@ -173,8 +173,8 @@
  78.155  
  78.156  local
  78.157  
  78.158 -fun hide_names command_spec what hide parse prep =
  78.159 -  Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
  78.160 +fun hide_names command_keyword what hide parse prep =
  78.161 +  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
  78.162      ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
  78.163        (Toplevel.theory (fn thy =>
  78.164          let val ctxt = Proof_Context.init_global thy
  78.165 @@ -183,19 +183,19 @@
  78.166  in
  78.167  
  78.168  val _ =
  78.169 -  hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
  78.170 +  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
  78.171      Proof_Context.read_class;
  78.172  
  78.173  val _ =
  78.174 -  hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
  78.175 +  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
  78.176      ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
  78.177  
  78.178  val _ =
  78.179 -  hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
  78.180 +  hide_names @{command_keyword hide_const} "constants" Sign.hide_const Parse.const
  78.181      ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
  78.182  
  78.183  val _ =
  78.184 -  hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
  78.185 +  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
  78.186      (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
  78.187  
  78.188  end;
  78.189 @@ -204,7 +204,7 @@
  78.190  (* use ML text *)
  78.191  
  78.192  val _ =
  78.193 -  Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
  78.194 +  Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
  78.195      (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
  78.196          let
  78.197            val ([{lines, pos, ...}], thy') = files thy;
  78.198 @@ -216,7 +216,7 @@
  78.199          end)));
  78.200  
  78.201  val _ =
  78.202 -  Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
  78.203 +  Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
  78.204      (Parse.ML_source >> (fn source =>
  78.205        let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
  78.206          Toplevel.theory
  78.207 @@ -224,7 +224,7 @@
  78.208        end));
  78.209  
  78.210  val _ =
  78.211 -  Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
  78.212 +  Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
  78.213      (Parse.ML_source >> (fn source =>
  78.214        let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
  78.215          Toplevel.generic_theory
  78.216 @@ -233,7 +233,7 @@
  78.217        end));
  78.218  
  78.219  val _ =
  78.220 -  Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
  78.221 +  Outer_Syntax.command @{command_keyword ML} "ML text within theory or local theory"
  78.222      (Parse.ML_source >> (fn source =>
  78.223        Toplevel.generic_theory
  78.224          (ML_Context.exec (fn () =>
  78.225 @@ -241,7 +241,7 @@
  78.226            Local_Theory.propagate_ml_env)));
  78.227  
  78.228  val _ =
  78.229 -  Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
  78.230 +  Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
  78.231      (Parse.ML_source >> (fn source =>
  78.232        Toplevel.proof (Proof.map_context (Context.proof_map
  78.233          (ML_Context.exec (fn () =>
  78.234 @@ -249,45 +249,45 @@
  78.235            Proof.propagate_ml_env)));
  78.236  
  78.237  val _ =
  78.238 -  Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
  78.239 +  Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
  78.240      (Parse.ML_source >> Isar_Cmd.ml_diag true);
  78.241  
  78.242  val _ =
  78.243 -  Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
  78.244 +  Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
  78.245      (Parse.ML_source >> Isar_Cmd.ml_diag false);
  78.246  
  78.247  val _ =
  78.248 -  Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
  78.249 -    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
  78.250 +  Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
  78.251 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
  78.252  
  78.253  val _ =
  78.254 -  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
  78.255 +  Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
  78.256      (Parse.ML_source >> Isar_Cmd.local_setup);
  78.257  
  78.258  val _ =
  78.259 -  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
  78.260 +  Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
  78.261      (Parse.position Parse.name --
  78.262          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
  78.263        >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
  78.264  
  78.265  val _ =
  78.266 -  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
  78.267 +  Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
  78.268      (Parse.position Parse.name --
  78.269          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
  78.270        >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
  78.271  
  78.272  val _ =
  78.273 -  Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
  78.274 +  Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
  78.275      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  78.276        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
  78.277  
  78.278  val _ =
  78.279 -  Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
  78.280 +  Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
  78.281      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  78.282        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
  78.283  
  78.284  val _ =
  78.285 -  Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
  78.286 +  Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
  78.287      (Parse.position Parse.name --
  78.288        (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
  78.289        Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
  78.290 @@ -297,27 +297,27 @@
  78.291  (* translation functions *)
  78.292  
  78.293  val _ =
  78.294 -  Outer_Syntax.command @{command_spec "parse_ast_translation"}
  78.295 +  Outer_Syntax.command @{command_keyword parse_ast_translation}
  78.296      "install parse ast translation functions"
  78.297      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
  78.298  
  78.299  val _ =
  78.300 -  Outer_Syntax.command @{command_spec "parse_translation"}
  78.301 +  Outer_Syntax.command @{command_keyword parse_translation}
  78.302      "install parse translation functions"
  78.303      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
  78.304  
  78.305  val _ =
  78.306 -  Outer_Syntax.command @{command_spec "print_translation"}
  78.307 +  Outer_Syntax.command @{command_keyword print_translation}
  78.308      "install print translation functions"
  78.309      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
  78.310  
  78.311  val _ =
  78.312 -  Outer_Syntax.command @{command_spec "typed_print_translation"}
  78.313 +  Outer_Syntax.command @{command_keyword typed_print_translation}
  78.314      "install typed print translation functions"
  78.315      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
  78.316  
  78.317  val _ =
  78.318 -  Outer_Syntax.command @{command_spec "print_ast_translation"}
  78.319 +  Outer_Syntax.command @{command_keyword print_ast_translation}
  78.320      "install print ast translation functions"
  78.321      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
  78.322  
  78.323 @@ -325,7 +325,7 @@
  78.324  (* oracles *)
  78.325  
  78.326  val _ =
  78.327 -  Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
  78.328 +  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
  78.329      (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
  78.330        (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
  78.331  
  78.332 @@ -333,22 +333,22 @@
  78.333  (* bundled declarations *)
  78.334  
  78.335  val _ =
  78.336 -  Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
  78.337 +  Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
  78.338      ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
  78.339        >> (uncurry Bundle.bundle_cmd));
  78.340  
  78.341  val _ =
  78.342 -  Outer_Syntax.command @{command_spec "include"}
  78.343 +  Outer_Syntax.command @{command_keyword include}
  78.344      "include declarations from bundle in proof body"
  78.345      (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
  78.346  
  78.347  val _ =
  78.348 -  Outer_Syntax.command @{command_spec "including"}
  78.349 +  Outer_Syntax.command @{command_keyword including}
  78.350      "include declarations from bundle in goal refinement"
  78.351      (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
  78.352  
  78.353  val _ =
  78.354 -  Outer_Syntax.command @{command_spec "print_bundles"}
  78.355 +  Outer_Syntax.command @{command_keyword print_bundles}
  78.356      "print bundles of declarations"
  78.357      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.358        Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
  78.359 @@ -357,7 +357,7 @@
  78.360  (* local theories *)
  78.361  
  78.362  val _ =
  78.363 -  Outer_Syntax.command @{command_spec "context"} "begin local theory context"
  78.364 +  Outer_Syntax.command @{command_keyword context} "begin local theory context"
  78.365      ((Parse.position Parse.xname >> (fn name =>
  78.366          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
  78.367        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
  78.368 @@ -373,7 +373,7 @@
  78.369    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
  78.370  
  78.371  val _ =
  78.372 -  Outer_Syntax.command @{command_spec "locale"} "define named specification context"
  78.373 +  Outer_Syntax.command @{command_keyword locale} "define named specification context"
  78.374      (Parse.binding --
  78.375        Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
  78.376        >> (fn ((name, (expr, elems)), begin) =>
  78.377 @@ -381,7 +381,7 @@
  78.378              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
  78.379  
  78.380  val _ =
  78.381 -  Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
  78.382 +  Outer_Syntax.command @{command_keyword experiment} "open private specification context"
  78.383      (Scan.repeat Parse_Spec.context_element --| Parse.begin
  78.384        >> (fn elems =>
  78.385            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
  78.386 @@ -392,7 +392,7 @@
  78.387        (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
  78.388  
  78.389  val _ =
  78.390 -  Outer_Syntax.command @{command_spec "sublocale"}
  78.391 +  Outer_Syntax.command @{command_keyword sublocale}
  78.392      "prove sublocale relation between a locale and a locale expression"
  78.393      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
  78.394        interpretation_args false >> (fn (loc, (expr, equations)) =>
  78.395 @@ -401,13 +401,13 @@
  78.396          Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
  78.397  
  78.398  val _ =
  78.399 -  Outer_Syntax.command @{command_spec "interpretation"}
  78.400 +  Outer_Syntax.command @{command_keyword interpretation}
  78.401      "prove interpretation of locale expression in local theory"
  78.402      (interpretation_args true >> (fn (expr, equations) =>
  78.403        Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
  78.404  
  78.405  val _ =
  78.406 -  Outer_Syntax.command @{command_spec "interpret"}
  78.407 +  Outer_Syntax.command @{command_keyword interpret}
  78.408      "prove interpretation of locale expression in proof context"
  78.409      (interpretation_args true >> (fn (expr, equations) =>
  78.410        Toplevel.proof' (Expression.interpret_cmd expr equations)));
  78.411 @@ -421,23 +421,23 @@
  78.412    Scan.repeat1 Parse_Spec.context_element >> pair [];
  78.413  
  78.414  val _ =
  78.415 -  Outer_Syntax.command @{command_spec "class"} "define type class"
  78.416 +  Outer_Syntax.command @{command_keyword class} "define type class"
  78.417     (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
  78.418      >> (fn ((name, (supclasses, elems)), begin) =>
  78.419          Toplevel.begin_local_theory begin
  78.420            (Class_Declaration.class_cmd name supclasses elems #> snd)));
  78.421  
  78.422  val _ =
  78.423 -  Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
  78.424 +  Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
  78.425      (Parse.class >> Class_Declaration.subclass_cmd);
  78.426  
  78.427  val _ =
  78.428 -  Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
  78.429 +  Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
  78.430     (Parse.multi_arity --| Parse.begin
  78.431       >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
  78.432  
  78.433  val _ =
  78.434 -  Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
  78.435 +  Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
  78.436    ((Parse.class --
  78.437      ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
  78.438      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
  78.439 @@ -447,7 +447,7 @@
  78.440  (* arbitrary overloading *)
  78.441  
  78.442  val _ =
  78.443 -  Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
  78.444 +  Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
  78.445     (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
  78.446        Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
  78.447        >> Parse.triple1) --| Parse.begin
  78.448 @@ -457,7 +457,7 @@
  78.449  (* code generation *)
  78.450  
  78.451  val _ =
  78.452 -  Outer_Syntax.command @{command_spec "code_datatype"}
  78.453 +  Outer_Syntax.command @{command_keyword code_datatype}
  78.454      "define set of code datatype constructors"
  78.455      (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
  78.456  
  78.457 @@ -478,32 +478,32 @@
  78.458          ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
  78.459            kind NONE (K I) a includes elems concl)));
  78.460  
  78.461 -val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
  78.462 -val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
  78.463 -val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
  78.464 -val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
  78.465 -val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
  78.466 -val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
  78.467 +val _ = theorem @{command_keyword theorem} false Thm.theoremK;
  78.468 +val _ = theorem @{command_keyword lemma} false Thm.lemmaK;
  78.469 +val _ = theorem @{command_keyword corollary} false Thm.corollaryK;
  78.470 +val _ = theorem @{command_keyword schematic_theorem} true Thm.theoremK;
  78.471 +val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
  78.472 +val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
  78.473  
  78.474  val _ =
  78.475 -  Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
  78.476 +  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
  78.477      (Parse.begin >> K Proof.begin_notepad);
  78.478  
  78.479  val _ =
  78.480 -  Outer_Syntax.command @{command_spec "have"} "state local goal"
  78.481 +  Outer_Syntax.command @{command_keyword have} "state local goal"
  78.482      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
  78.483  
  78.484  val _ =
  78.485 -  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
  78.486 +  Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
  78.487      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
  78.488  
  78.489  val _ =
  78.490 -  Outer_Syntax.command @{command_spec "show"}
  78.491 +  Outer_Syntax.command @{command_keyword show}
  78.492      "state local goal, solving current obligation"
  78.493      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
  78.494  
  78.495  val _ =
  78.496 -  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
  78.497 +  Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
  78.498      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
  78.499  
  78.500  
  78.501 @@ -512,46 +512,46 @@
  78.502  val facts = Parse.and_list1 Parse.xthms1;
  78.503  
  78.504  val _ =
  78.505 -  Outer_Syntax.command @{command_spec "then"} "forward chaining"
  78.506 +  Outer_Syntax.command @{command_keyword then} "forward chaining"
  78.507      (Scan.succeed (Toplevel.proof Proof.chain));
  78.508  
  78.509  val _ =
  78.510 -  Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
  78.511 +  Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
  78.512      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
  78.513  
  78.514  val _ =
  78.515 -  Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
  78.516 +  Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
  78.517      (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
  78.518  
  78.519  val _ =
  78.520 -  Outer_Syntax.command @{command_spec "note"} "define facts"
  78.521 +  Outer_Syntax.command @{command_keyword note} "define facts"
  78.522      (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
  78.523  
  78.524  val _ =
  78.525 -  Outer_Syntax.command @{command_spec "using"} "augment goal facts"
  78.526 +  Outer_Syntax.command @{command_keyword using} "augment goal facts"
  78.527      (facts >> (Toplevel.proof o Proof.using_cmd));
  78.528  
  78.529  val _ =
  78.530 -  Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
  78.531 +  Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
  78.532      (facts >> (Toplevel.proof o Proof.unfolding_cmd));
  78.533  
  78.534  
  78.535  (* proof context *)
  78.536  
  78.537  val _ =
  78.538 -  Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
  78.539 +  Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
  78.540      (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
  78.541  
  78.542  val _ =
  78.543 -  Outer_Syntax.command @{command_spec "assume"} "assume propositions"
  78.544 +  Outer_Syntax.command @{command_keyword assume} "assume propositions"
  78.545      (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
  78.546  
  78.547  val _ =
  78.548 -  Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
  78.549 +  Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
  78.550      (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
  78.551  
  78.552  val _ =
  78.553 -  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
  78.554 +  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
  78.555      (Parse.and_list1
  78.556        (Parse_Spec.opt_thm_name ":" --
  78.557          ((Parse.binding -- Parse.opt_mixfix) --
  78.558 @@ -559,26 +559,26 @@
  78.559      >> (Toplevel.proof o Proof.def_cmd));
  78.560  
  78.561  val _ =
  78.562 -  Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
  78.563 +  Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
  78.564      (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
  78.565        >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
  78.566  
  78.567  val _ =
  78.568 -  Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
  78.569 +  Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
  78.570      (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
  78.571  
  78.572  val _ =
  78.573 -  Outer_Syntax.command @{command_spec "let"} "bind text variables"
  78.574 +  Outer_Syntax.command @{command_keyword let} "bind text variables"
  78.575      (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
  78.576        >> (Toplevel.proof o Proof.let_bind_cmd));
  78.577  
  78.578  val _ =
  78.579 -  Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
  78.580 +  Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
  78.581      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  78.582      >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
  78.583  
  78.584  val _ =
  78.585 -  Outer_Syntax.command @{command_spec "case"} "invoke local context"
  78.586 +  Outer_Syntax.command @{command_keyword case} "invoke local context"
  78.587      ((@{keyword "("} |--
  78.588        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
  78.589          --| @{keyword ")"}) ||
  78.590 @@ -589,74 +589,74 @@
  78.591  (* proof structure *)
  78.592  
  78.593  val _ =
  78.594 -  Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
  78.595 +  Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
  78.596      (Scan.succeed (Toplevel.proof Proof.begin_block));
  78.597  
  78.598  val _ =
  78.599 -  Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
  78.600 +  Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
  78.601      (Scan.succeed (Toplevel.proof Proof.end_block));
  78.602  
  78.603  val _ =
  78.604 -  Outer_Syntax.command @{command_spec "next"} "enter next proof block"
  78.605 +  Outer_Syntax.command @{command_keyword next} "enter next proof block"
  78.606      (Scan.succeed (Toplevel.proof Proof.next_block));
  78.607  
  78.608  
  78.609  (* end proof *)
  78.610  
  78.611  val _ =
  78.612 -  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
  78.613 +  Outer_Syntax.command @{command_keyword qed} "conclude proof"
  78.614      (Scan.option Method.parse >> (fn m =>
  78.615       (Option.map Method.report m;
  78.616        Isar_Cmd.qed m)));
  78.617  
  78.618  val _ =
  78.619 -  Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
  78.620 +  Outer_Syntax.command @{command_keyword by} "terminal backward proof"
  78.621      (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
  78.622       (Method.report m1;
  78.623        Option.map Method.report m2;
  78.624        Isar_Cmd.terminal_proof (m1, m2))));
  78.625  
  78.626  val _ =
  78.627 -  Outer_Syntax.command @{command_spec ".."} "default proof"
  78.628 +  Outer_Syntax.command @{command_keyword ".."} "default proof"
  78.629      (Scan.succeed Isar_Cmd.default_proof);
  78.630  
  78.631  val _ =
  78.632 -  Outer_Syntax.command @{command_spec "."} "immediate proof"
  78.633 +  Outer_Syntax.command @{command_keyword "."} "immediate proof"
  78.634      (Scan.succeed Isar_Cmd.immediate_proof);
  78.635  
  78.636  val _ =
  78.637 -  Outer_Syntax.command @{command_spec "done"} "done proof"
  78.638 +  Outer_Syntax.command @{command_keyword done} "done proof"
  78.639      (Scan.succeed Isar_Cmd.done_proof);
  78.640  
  78.641  val _ =
  78.642 -  Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
  78.643 +  Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
  78.644      (Scan.succeed Isar_Cmd.skip_proof);
  78.645  
  78.646  val _ =
  78.647 -  Outer_Syntax.command @{command_spec "oops"} "forget proof"
  78.648 +  Outer_Syntax.command @{command_keyword oops} "forget proof"
  78.649      (Scan.succeed (Toplevel.forget_proof true));
  78.650  
  78.651  
  78.652  (* proof steps *)
  78.653  
  78.654  val _ =
  78.655 -  Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
  78.656 +  Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
  78.657      (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
  78.658  
  78.659  val _ =
  78.660 -  Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
  78.661 +  Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
  78.662      (Parse.nat >> (Toplevel.proof o Proof.prefer));
  78.663  
  78.664  val _ =
  78.665 -  Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
  78.666 +  Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
  78.667      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
  78.668  
  78.669  val _ =
  78.670 -  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
  78.671 +  Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
  78.672      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
  78.673  
  78.674  val _ =
  78.675 -  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
  78.676 +  Outer_Syntax.command @{command_keyword proof} "backward proof step"
  78.677      (Scan.option Method.parse >> (fn m =>
  78.678        (Option.map Method.report m;
  78.679          Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
  78.680 @@ -669,7 +669,7 @@
  78.681    Output.report [Markup.markup Markup.bad "Explicit backtracking"];
  78.682  
  78.683  val _ =
  78.684 -  Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
  78.685 +  Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
  78.686      (Scan.succeed
  78.687       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  78.688        Toplevel.skip_proof (fn h => (report_back (); h))));
  78.689 @@ -682,194 +682,194 @@
  78.690    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
  78.691  
  78.692  val _ =
  78.693 -  Outer_Syntax.command @{command_spec "help"}
  78.694 +  Outer_Syntax.command @{command_keyword help}
  78.695      "retrieve outer syntax commands according to name patterns"
  78.696      (Scan.repeat Parse.name >>
  78.697        (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  78.698  
  78.699  val _ =
  78.700 -  Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
  78.701 +  Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
  78.702      (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  78.703  
  78.704  val _ =
  78.705 -  Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
  78.706 +  Outer_Syntax.command @{command_keyword print_options} "print configuration options"
  78.707      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.708        Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  78.709  
  78.710  val _ =
  78.711 -  Outer_Syntax.command @{command_spec "print_context"}
  78.712 +  Outer_Syntax.command @{command_keyword print_context}
  78.713      "print context of local theory target"
  78.714      (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  78.715  
  78.716  val _ =
  78.717 -  Outer_Syntax.command @{command_spec "print_theory"}
  78.718 +  Outer_Syntax.command @{command_keyword print_theory}
  78.719      "print logical theory contents"
  78.720      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  78.721        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
  78.722  
  78.723  val _ =
  78.724 -  Outer_Syntax.command @{command_spec "print_syntax"}
  78.725 +  Outer_Syntax.command @{command_keyword print_syntax}
  78.726      "print inner syntax of context"
  78.727      (Scan.succeed (Toplevel.unknown_context o
  78.728        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  78.729  
  78.730  val _ =
  78.731 -  Outer_Syntax.command @{command_spec "print_defn_rules"}
  78.732 +  Outer_Syntax.command @{command_keyword print_defn_rules}
  78.733      "print definitional rewrite rules of context"
  78.734      (Scan.succeed (Toplevel.unknown_context o
  78.735        Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  78.736  
  78.737  val _ =
  78.738 -  Outer_Syntax.command @{command_spec "print_abbrevs"}
  78.739 +  Outer_Syntax.command @{command_keyword print_abbrevs}
  78.740      "print constant abbreviations of context"
  78.741      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.742        Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  78.743  
  78.744  val _ =
  78.745 -  Outer_Syntax.command @{command_spec "print_theorems"}
  78.746 +  Outer_Syntax.command @{command_keyword print_theorems}
  78.747      "print theorems of local theory or proof context"
  78.748      (Parse.opt_bang >> (fn b =>
  78.749        Toplevel.unknown_context o
  78.750        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  78.751  
  78.752  val _ =
  78.753 -  Outer_Syntax.command @{command_spec "print_locales"}
  78.754 +  Outer_Syntax.command @{command_keyword print_locales}
  78.755      "print locales of this theory"
  78.756      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  78.757        Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  78.758  
  78.759  val _ =
  78.760 -  Outer_Syntax.command @{command_spec "print_classes"}
  78.761 +  Outer_Syntax.command @{command_keyword print_classes}
  78.762      "print classes of this theory"
  78.763      (Scan.succeed (Toplevel.unknown_theory o
  78.764        Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  78.765  
  78.766  val _ =
  78.767 -  Outer_Syntax.command @{command_spec "print_locale"}
  78.768 +  Outer_Syntax.command @{command_keyword print_locale}
  78.769      "print locale of this theory"
  78.770      (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
  78.771        Toplevel.unknown_theory o
  78.772        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  78.773  
  78.774  val _ =
  78.775 -  Outer_Syntax.command @{command_spec "print_interps"}
  78.776 +  Outer_Syntax.command @{command_keyword print_interps}
  78.777      "print interpretations of locale for this theory or proof context"
  78.778      (Parse.position Parse.xname >> (fn name =>
  78.779        Toplevel.unknown_context o
  78.780        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  78.781  
  78.782  val _ =
  78.783 -  Outer_Syntax.command @{command_spec "print_dependencies"}
  78.784 +  Outer_Syntax.command @{command_keyword print_dependencies}
  78.785      "print dependencies of locale expression"
  78.786      (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
  78.787        Toplevel.unknown_context o
  78.788        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  78.789  
  78.790  val _ =
  78.791 -  Outer_Syntax.command @{command_spec "print_attributes"}
  78.792 +  Outer_Syntax.command @{command_keyword print_attributes}
  78.793      "print attributes of this theory"
  78.794      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  78.795        Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  78.796  
  78.797  val _ =
  78.798 -  Outer_Syntax.command @{command_spec "print_simpset"}
  78.799 +  Outer_Syntax.command @{command_keyword print_simpset}
  78.800      "print context of Simplifier"
  78.801      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.802        Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  78.803  
  78.804  val _ =
  78.805 -  Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
  78.806 +  Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
  78.807      (Scan.succeed (Toplevel.unknown_context o
  78.808        Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  78.809  
  78.810  val _ =
  78.811 -  Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
  78.812 +  Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
  78.813      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  78.814        Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  78.815  
  78.816  val _ =
  78.817 -  Outer_Syntax.command @{command_spec "print_antiquotations"}
  78.818 +  Outer_Syntax.command @{command_keyword print_antiquotations}
  78.819      "print document antiquotations"
  78.820      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.821        Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
  78.822  
  78.823  val _ =
  78.824 -  Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
  78.825 +  Outer_Syntax.command @{command_keyword print_ML_antiquotations}
  78.826      "print ML antiquotations"
  78.827      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.828        Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  78.829  
  78.830  val _ =
  78.831 -  Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
  78.832 +  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  78.833      (Scan.succeed Isar_Cmd.thy_deps);
  78.834  
  78.835  val _ =
  78.836 -  Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
  78.837 +  Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
  78.838      (Scan.succeed Isar_Cmd.locale_deps);
  78.839  
  78.840  val _ =
  78.841 -  Outer_Syntax.command @{command_spec "print_term_bindings"}
  78.842 +  Outer_Syntax.command @{command_keyword print_term_bindings}
  78.843      "print term bindings of proof context"
  78.844      (Scan.succeed (Toplevel.unknown_context o
  78.845        Toplevel.keep
  78.846          (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  78.847  
  78.848  val _ =
  78.849 -  Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
  78.850 +  Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
  78.851      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  78.852        Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  78.853  
  78.854  val _ =
  78.855 -  Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
  78.856 +  Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
  78.857      (Scan.succeed (Toplevel.unknown_context o
  78.858        Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  78.859  
  78.860  val _ =
  78.861 -  Outer_Syntax.command @{command_spec "print_statement"}
  78.862 +  Outer_Syntax.command @{command_keyword print_statement}
  78.863      "print theorems as long statements"
  78.864      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
  78.865  
  78.866  val _ =
  78.867 -  Outer_Syntax.command @{command_spec "thm"} "print theorems"
  78.868 +  Outer_Syntax.command @{command_keyword thm} "print theorems"
  78.869      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
  78.870  
  78.871  val _ =
  78.872 -  Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
  78.873 +  Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
  78.874      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
  78.875  
  78.876  val _ =
  78.877 -  Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
  78.878 +  Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
  78.879      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
  78.880  
  78.881  val _ =
  78.882 -  Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
  78.883 +  Outer_Syntax.command @{command_keyword prop} "read and print proposition"
  78.884      (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  78.885  
  78.886  val _ =
  78.887 -  Outer_Syntax.command @{command_spec "term"} "read and print term"
  78.888 +  Outer_Syntax.command @{command_keyword term} "read and print term"
  78.889      (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  78.890  
  78.891  val _ =
  78.892 -  Outer_Syntax.command @{command_spec "typ"} "read and print type"
  78.893 +  Outer_Syntax.command @{command_keyword typ} "read and print type"
  78.894      (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
  78.895        >> Isar_Cmd.print_type);
  78.896  
  78.897  val _ =
  78.898 -  Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
  78.899 +  Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
  78.900      (Scan.succeed (Toplevel.unknown_theory o
  78.901        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  78.902  
  78.903  val _ =
  78.904 -  Outer_Syntax.command @{command_spec "print_state"}
  78.905 +  Outer_Syntax.command @{command_keyword print_state}
  78.906      "print current proof state (if present)"
  78.907      (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
  78.908  
  78.909  val _ =
  78.910 -  Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
  78.911 +  Outer_Syntax.command @{command_keyword welcome} "print welcome message"
  78.912      (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
  78.913  
  78.914  val _ =
  78.915 -  Outer_Syntax.command @{command_spec "display_drafts"}
  78.916 +  Outer_Syntax.command @{command_keyword display_drafts}
  78.917      "display raw source files with symbols"
  78.918      (Scan.repeat1 Parse.path >> (fn names =>
  78.919        Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
  78.920 @@ -881,24 +881,24 @@
  78.921  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  78.922  
  78.923  val _ =
  78.924 -  Outer_Syntax.command @{command_spec "realizers"}
  78.925 +  Outer_Syntax.command @{command_keyword realizers}
  78.926      "specify realizers for primitive axioms / theorems, together with correctness proof"
  78.927      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  78.928       (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  78.929         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  78.930  
  78.931  val _ =
  78.932 -  Outer_Syntax.command @{command_spec "realizability"}
  78.933 +  Outer_Syntax.command @{command_keyword realizability}
  78.934      "add equations characterizing realizability"
  78.935      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  78.936  
  78.937  val _ =
  78.938 -  Outer_Syntax.command @{command_spec "extract_type"}
  78.939 +  Outer_Syntax.command @{command_keyword extract_type}
  78.940      "add equations characterizing type of extracted program"
  78.941      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  78.942  
  78.943  val _ =
  78.944 -  Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
  78.945 +  Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  78.946      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  78.947        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  78.948  
  78.949 @@ -907,10 +907,9 @@
  78.950  (** end **)
  78.951  
  78.952  val _ =
  78.953 -  Outer_Syntax.command @{command_spec "end"} "end context"
  78.954 +  Outer_Syntax.command @{command_keyword end} "end context"
  78.955      (Scan.succeed
  78.956        (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
  78.957          Toplevel.end_proof (K Proof.end_notepad)));
  78.958  
  78.959  end;
  78.960 -
    79.1 --- a/src/Pure/Isar/keyword.ML	Mon Apr 06 15:23:50 2015 +0200
    79.2 +++ b/src/Pure/Isar/keyword.ML	Mon Apr 06 23:24:45 2015 +0200
    79.3 @@ -37,10 +37,11 @@
    79.4    val no_command_keywords: keywords -> keywords
    79.5    val empty_keywords: keywords
    79.6    val merge_keywords: keywords * keywords -> keywords
    79.7 -  val add_keywords: (string * spec option) list -> keywords -> keywords
    79.8 +  val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
    79.9    val is_keyword: keywords -> string -> bool
   79.10    val is_command: keywords -> string -> bool
   79.11    val is_literal: keywords -> string -> bool
   79.12 +  val command_markup: keywords -> string -> Markup.T option
   79.13    val command_kind: keywords -> string -> string option
   79.14    val command_files: keywords -> string -> Path.T -> Path.T list
   79.15    val command_tags: keywords -> string -> string list
   79.16 @@ -105,19 +106,21 @@
   79.17  
   79.18  (* specifications *)
   79.19  
   79.20 -type T =
   79.21 - {kind: string,
   79.22 +type spec = (string * string list) * string list;
   79.23 +
   79.24 +type entry =
   79.25 + {pos: Position.T,
   79.26 +  id: serial,
   79.27 +  kind: string,
   79.28    files: string list,  (*extensions of embedded files*)
   79.29    tags: string list};
   79.30  
   79.31 -type spec = (string * string list) * string list;
   79.32 -
   79.33 -fun check_spec ((kind, files), tags) : T =
   79.34 +fun check_spec pos ((kind, files), tags) : entry =
   79.35    if not (member (op =) kinds kind) then
   79.36      error ("Unknown outer syntax keyword kind " ^ quote kind)
   79.37    else if not (null files) andalso kind <> thy_load then
   79.38      error ("Illegal specification of files for " ^ quote kind)
   79.39 -  else {kind = kind, files = files, tags = tags};
   79.40 +  else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
   79.41  
   79.42  
   79.43  
   79.44 @@ -128,7 +131,7 @@
   79.45  datatype keywords = Keywords of
   79.46   {minor: Scan.lexicon,
   79.47    major: Scan.lexicon,
   79.48 -  commands: T Symtab.table};
   79.49 +  commands: entry Symtab.table};
   79.50  
   79.51  fun minor_keywords (Keywords {minor, ...}) = minor;
   79.52  fun major_keywords (Keywords {major, ...}) = major;
   79.53 @@ -157,7 +160,7 @@
   79.54      Symtab.merge (K true) (commands1, commands2));
   79.55  
   79.56  val add_keywords =
   79.57 -  fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
   79.58 +  fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
   79.59      (case opt_spec of
   79.60        NONE =>
   79.61          let
   79.62 @@ -165,9 +168,9 @@
   79.63          in (minor', major, commands) end
   79.64      | SOME spec =>
   79.65          let
   79.66 -          val kind = check_spec spec;
   79.67 +          val entry = check_spec pos spec;
   79.68            val major' = Scan.extend_lexicon (Symbol.explode name) major;
   79.69 -          val commands' = Symtab.update (name, kind) commands;
   79.70 +          val commands' = Symtab.update (name, entry) commands;
   79.71          in (minor, major', commands') end)));
   79.72  
   79.73  
   79.74 @@ -178,10 +181,16 @@
   79.75  fun is_literal keywords = is_keyword keywords orf is_command keywords;
   79.76  
   79.77  
   79.78 -(* command kind *)
   79.79 +(* command keywords *)
   79.80  
   79.81  fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
   79.82  
   79.83 +fun command_markup keywords name =
   79.84 +  lookup_command keywords name
   79.85 +  |> Option.map (fn {pos, id, ...} =>
   79.86 +      Markup.properties (Position.entity_properties_of false id pos)
   79.87 +        (Markup.entity Markup.command_keywordN name));
   79.88 +
   79.89  fun command_kind keywords = Option.map #kind o lookup_command keywords;
   79.90  
   79.91  fun command_files keywords name path =
    80.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 15:23:50 2015 +0200
    80.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 23:24:45 2015 +0200
    80.3 @@ -8,16 +8,16 @@
    80.4  sig
    80.5    val help: theory -> string list -> unit
    80.6    val print_commands: theory -> unit
    80.7 -  type command_spec = string * Position.T
    80.8 -  val command: command_spec -> string ->
    80.9 +  type command_keyword = string * Position.T
   80.10 +  val command: command_keyword -> string ->
   80.11      (Toplevel.transition -> Toplevel.transition) parser -> unit
   80.12 -  val local_theory': command_spec -> string ->
   80.13 +  val local_theory': command_keyword -> string ->
   80.14      (bool -> local_theory -> local_theory) parser -> unit
   80.15 -  val local_theory: command_spec -> string ->
   80.16 +  val local_theory: command_keyword -> string ->
   80.17      (local_theory -> local_theory) parser -> unit
   80.18 -  val local_theory_to_proof': command_spec -> string ->
   80.19 +  val local_theory_to_proof': command_keyword -> string ->
   80.20      (bool -> local_theory -> Proof.state) parser -> unit
   80.21 -  val local_theory_to_proof: command_spec -> string ->
   80.22 +  val local_theory_to_proof: command_keyword -> string ->
   80.23      (local_theory -> Proof.state) parser -> unit
   80.24    val parse: theory -> Position.T -> string -> Toplevel.transition list
   80.25    val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   80.26 @@ -44,7 +44,8 @@
   80.27  
   80.28  datatype command_parser =
   80.29    Parser of (Toplevel.transition -> Toplevel.transition) parser |
   80.30 -  Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser;
   80.31 +  Limited_Parser of
   80.32 +    (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
   80.33  
   80.34  datatype command = Command of
   80.35   {comment: string,
   80.36 @@ -134,18 +135,19 @@
   80.37  
   80.38  (* implicit theory setup *)
   80.39  
   80.40 -type command_spec = string * Position.T;
   80.41 +type command_keyword = string * Position.T;
   80.42  
   80.43  fun raw_command (name, pos) comment command_parser =
   80.44 -  Theory.setup (add_command name (new_command comment command_parser pos));
   80.45 +  let val setup = add_command name (new_command comment command_parser pos)
   80.46 +  in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
   80.47  
   80.48  fun command (name, pos) comment parse =
   80.49    raw_command (name, pos) comment (Parser parse);
   80.50  
   80.51 -fun local_theory_command trans command_spec comment parse =
   80.52 -  raw_command command_spec comment
   80.53 -    (Private_Parser (fn private =>
   80.54 -      Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
   80.55 +fun local_theory_command trans command_keyword comment parse =
   80.56 +  raw_command command_keyword comment
   80.57 +    (Limited_Parser (fn limited =>
   80.58 +      Parse.opt_target -- parse >> (fn (target, f) => trans limited target f)));
   80.59  
   80.60  val local_theory' = local_theory_command Toplevel.local_theory';
   80.61  val local_theory = local_theory_command Toplevel.local_theory;
   80.62 @@ -160,8 +162,11 @@
   80.63  
   80.64  local
   80.65  
   80.66 +val before_command =
   80.67 +  Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
   80.68 +
   80.69  fun parse_command thy =
   80.70 -  Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
   80.71 +  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
   80.72      let
   80.73        val command_tags = Parse.command_ -- Parse.tags;
   80.74        val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
   80.75 @@ -169,9 +174,9 @@
   80.76        (case lookup_commands thy name of
   80.77          SOME (Command {command_parser = Parser parse, ...}) =>
   80.78            Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
   80.79 -      | SOME (Command {command_parser = Private_Parser parse, ...}) =>
   80.80 -          Parse.opt_private :|-- (fn private =>
   80.81 -            Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0)
   80.82 +      | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
   80.83 +          before_command :|-- (fn limited =>
   80.84 +            Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
   80.85        | NONE =>
   80.86            Scan.succeed
   80.87              (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
   80.88 @@ -224,9 +229,9 @@
   80.89  
   80.90  fun parse tok (result, content, improper) =
   80.91    if Token.is_improper tok then (result, content, tok :: improper)
   80.92 -  else if Token.is_private tok orelse
   80.93 +  else if Token.is_command_modifier tok orelse
   80.94      Token.is_command tok andalso
   80.95 -      (not (exists Token.is_private content) orelse exists Token.is_command content)
   80.96 +      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
   80.97    then (flush (result, content, improper), [tok], [])
   80.98    else (result, tok :: (improper @ content), []);
   80.99  
    81.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 15:23:50 2015 +0200
    81.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 23:24:45 2015 +0200
    81.3 @@ -219,8 +219,8 @@
    81.4  
    81.5      for (tok <- toks) {
    81.6        if (tok.is_improper) improper += tok
    81.7 -      else if (tok.is_private ||
    81.8 -        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
    81.9 +      else if (tok.is_command_modifier ||
   81.10 +        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
   81.11        { flush(); content += tok }
   81.12        else { content ++= improper; improper.clear; content += tok }
   81.13      }
    82.1 --- a/src/Pure/Isar/parse.ML	Mon Apr 06 15:23:50 2015 +0200
    82.2 +++ b/src/Pure/Isar/parse.ML	Mon Apr 06 23:24:45 2015 +0200
    82.3 @@ -104,7 +104,7 @@
    82.4    val propp: (string * string list) parser
    82.5    val termp: (string * string list) parser
    82.6    val private: Position.T parser
    82.7 -  val opt_private: Position.T option parser
    82.8 +  val restricted: Position.T parser
    82.9    val target: (xstring * Position.T) parser
   82.10    val opt_target: (xstring * Position.T) option parser
   82.11    val args: Token.T list parser
   82.12 @@ -401,7 +401,7 @@
   82.13  (* target information *)
   82.14  
   82.15  val private = position ($$$ "private") >> #2;
   82.16 -val opt_private = Scan.option private;
   82.17 +val restricted = position ($$$ "restricted") >> #2;
   82.18  
   82.19  val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
   82.20  val opt_target = Scan.option target;
    83.1 --- a/src/Pure/Isar/proof_context.ML	Mon Apr 06 15:23:50 2015 +0200
    83.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Apr 06 23:24:45 2015 +0200
    83.3 @@ -38,6 +38,8 @@
    83.4    val new_scope: Proof.context -> Binding.scope * Proof.context
    83.5    val private_scope: Binding.scope -> Proof.context -> Proof.context
    83.6    val private: Position.T -> Proof.context -> Proof.context
    83.7 +  val restricted_scope: Binding.scope -> Proof.context -> Proof.context
    83.8 +  val restricted: Position.T -> Proof.context -> Proof.context
    83.9    val concealed: Proof.context -> Proof.context
   83.10    val class_space: Proof.context -> Name_Space.T
   83.11    val type_space: Proof.context -> Name_Space.T
   83.12 @@ -319,6 +321,9 @@
   83.13  
   83.14  val private_scope = map_naming o Name_Space.private_scope;
   83.15  val private = map_naming o Name_Space.private;
   83.16 +val restricted_scope = map_naming o Name_Space.restricted_scope;
   83.17 +val restricted = map_naming o Name_Space.restricted;
   83.18 +
   83.19  val concealed = map_naming Name_Space.concealed;
   83.20  
   83.21  
    84.1 --- a/src/Pure/Isar/token.ML	Mon Apr 06 15:23:50 2015 +0200
    84.2 +++ b/src/Pure/Isar/token.ML	Mon Apr 06 23:24:45 2015 +0200
    84.3 @@ -46,7 +46,7 @@
    84.4    val is_command: T -> bool
    84.5    val is_name: T -> bool
    84.6    val keyword_with: (string -> bool) -> T -> bool
    84.7 -  val is_private: T -> bool
    84.8 +  val is_command_modifier: T -> bool
    84.9    val ident_with: (string -> bool) -> T -> bool
   84.10    val is_proper: T -> bool
   84.11    val is_improper: T -> bool
   84.12 @@ -247,7 +247,7 @@
   84.13  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   84.14    | keyword_with _ _ = false;
   84.15  
   84.16 -val is_private = keyword_with (fn x => x = "private");
   84.17 +val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
   84.18  
   84.19  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   84.20    | ident_with _ _ = false;
    85.1 --- a/src/Pure/Isar/token.scala	Mon Apr 06 15:23:50 2015 +0200
    85.2 +++ b/src/Pure/Isar/token.scala	Mon Apr 06 23:24:45 2015 +0200
    85.3 @@ -259,7 +259,8 @@
    85.4    def is_begin: Boolean = is_keyword && source == "begin"
    85.5    def is_end: Boolean = is_command && source == "end"
    85.6  
    85.7 -  def is_private: Boolean = is_keyword && source == "private"
    85.8 +  def is_command_modifier: Boolean =
    85.9 +    is_keyword && (source == "private" || source == "restricted")
   85.10  
   85.11    def is_begin_block: Boolean = is_command && source == "{"
   85.12    def is_end_block: Boolean = is_command && source == "}"
    86.1 --- a/src/Pure/Isar/toplevel.ML	Mon Apr 06 15:23:50 2015 +0200
    86.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Apr 06 23:24:45 2015 +0200
    86.3 @@ -51,15 +51,15 @@
    86.4    val end_local_theory: transition -> transition
    86.5    val open_target: (generic_theory -> local_theory) -> transition -> transition
    86.6    val close_target: transition -> transition
    86.7 -  val local_theory': Position.T option -> (xstring * Position.T) option ->
    86.8 +  val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
    86.9      (bool -> local_theory -> local_theory) -> transition -> transition
   86.10 -  val local_theory: Position.T option -> (xstring * Position.T) option ->
   86.11 +  val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
   86.12      (local_theory -> local_theory) -> transition -> transition
   86.13    val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
   86.14      transition -> transition
   86.15 -  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
   86.16 +  val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
   86.17      (bool -> local_theory -> Proof.state) -> transition -> transition
   86.18 -  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
   86.19 +  val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option ->
   86.20      (local_theory -> Proof.state) -> transition -> transition
   86.21    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   86.22    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   86.23 @@ -412,12 +412,15 @@
   86.24          | NONE => raise UNDEF)
   86.25      | _ => raise UNDEF));
   86.26  
   86.27 -fun local_theory' private target f = present_transaction (fn int =>
   86.28 +val limited_context =
   86.29 +  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
   86.30 +
   86.31 +fun local_theory' limited target f = present_transaction (fn int =>
   86.32    (fn Theory (gthy, _) =>
   86.33          let
   86.34            val (finish, lthy) = Named_Target.switch target gthy;
   86.35            val lthy' = lthy
   86.36 -            |> fold Proof_Context.private (the_list private)
   86.37 +            |> limited_context limited
   86.38              |> Local_Theory.new_group
   86.39              |> f int
   86.40              |> Local_Theory.reset_group;
   86.41 @@ -425,7 +428,7 @@
   86.42      | _ => raise UNDEF))
   86.43    (K ());
   86.44  
   86.45 -fun local_theory private target f = local_theory' private target (K f);
   86.46 +fun local_theory limited target f = local_theory' limited target (K f);
   86.47  
   86.48  fun present_local_theory target = present_transaction (fn int =>
   86.49    (fn Theory (gthy, _) =>
   86.50 @@ -470,18 +473,18 @@
   86.51  
   86.52  in
   86.53  
   86.54 -fun local_theory_to_proof' private target f = begin_proof
   86.55 +fun local_theory_to_proof' limited target f = begin_proof
   86.56    (fn int => fn gthy =>
   86.57      let
   86.58        val (finish, lthy) = Named_Target.switch target gthy;
   86.59        val prf = lthy
   86.60 -        |> fold Proof_Context.private (the_list private)
   86.61 +        |> limited_context limited
   86.62          |> Local_Theory.new_group
   86.63          |> f int;
   86.64      in (finish o Local_Theory.reset_group, prf) end);
   86.65  
   86.66 -fun local_theory_to_proof private target f =
   86.67 -  local_theory_to_proof' private target (K f);
   86.68 +fun local_theory_to_proof limited target f =
   86.69 +  local_theory_to_proof' limited target (K f);
   86.70  
   86.71  fun theory_to_proof f = begin_proof
   86.72    (fn _ => fn gthy =>
    87.1 --- a/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 15:23:50 2015 +0200
    87.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 23:24:45 2015 +0200
    87.3 @@ -253,11 +253,12 @@
    87.4        if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
    87.5          "Parse.$$$ " ^ ML_Syntax.print_string name
    87.6        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    87.7 -  ML_Antiquotation.value @{binding command_spec}
    87.8 -    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
    87.9 -      if Keyword.is_command (Thy_Header.get_keywords thy) name then
   87.10 -        ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
   87.11 -      else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
   87.12 +  ML_Antiquotation.value @{binding command_keyword}
   87.13 +    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
   87.14 +      (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
   87.15 +        SOME markup =>
   87.16 +         (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
   87.17 +          ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
   87.18 +      | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
   87.19  
   87.20  end;
   87.21 -
    88.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 06 15:23:50 2015 +0200
    88.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 06 23:24:45 2015 +0200
    88.3 @@ -125,8 +125,8 @@
    88.4            NONE => I
    88.5          | SOME id => Protocol_Message.command_positions_yxml id)
    88.6          |> error;
    88.7 -    val {name = (name, _), imports, keywords} = header;
    88.8 -    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    88.9 +    val {name = (name, _), imports, ...} = header;
   88.10 +    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
   88.11    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
   88.12  
   88.13  fun get_perspective (Node {perspective, ...}) = perspective;
    89.1 --- a/src/Pure/PIDE/markup.ML	Mon Apr 06 15:23:50 2015 +0200
    89.2 +++ b/src/Pure/PIDE/markup.ML	Mon Apr 06 23:24:45 2015 +0200
    89.3 @@ -115,6 +115,7 @@
    89.4    val paragraphN: string val paragraph: T
    89.5    val text_foldN: string val text_fold: T
    89.6    val inputN: string val input: bool -> Properties.T -> T
    89.7 +  val command_keywordN: string val command_keyword: T
    89.8    val commandN: string val command: T
    89.9    val stringN: string val string: T
   89.10    val alt_stringN: string val alt_string: T
   89.11 @@ -464,6 +465,7 @@
   89.12  
   89.13  (* outer syntax *)
   89.14  
   89.15 +val (command_keywordN, command_keyword) = markup_elem "command_keyword";
   89.16  val (commandN, command) = markup_elem "command";
   89.17  val (keyword1N, keyword1) = markup_elem "keyword1";
   89.18  val (keyword2N, keyword2) = markup_elem "keyword2";
    90.1 --- a/src/Pure/PIDE/protocol.ML	Mon Apr 06 15:23:50 2015 +0200
    90.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 06 23:24:45 2015 +0200
    90.3 @@ -81,7 +81,8 @@
    90.4                                (option (pair (pair string (list string)) (list string)))))
    90.5                                (list YXML.string_of_body)))) a;
    90.6                          val imports' = map (rpair Position.none) imports;
    90.7 -                        val header = Thy_Header.make (name, Position.none) imports' keywords;
    90.8 +                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
    90.9 +                        val header = Thy_Header.make (name, Position.none) imports' keywords';
   90.10                        in Document.Deps {master = master, header = header, errors = errors} end,
   90.11                      fn (a :: b, c) =>
   90.12                        Document.Perspective (bool_atom a, map int_atom b,
    91.1 --- a/src/Pure/Pure.thy	Mon Apr 06 15:23:50 2015 +0200
    91.2 +++ b/src/Pure/Pure.thy	Mon Apr 06 23:24:45 2015 +0200
    91.3 @@ -11,8 +11,8 @@
    91.4      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    91.5      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    91.6      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    91.7 -    "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
    91.8 -    "where" "|"
    91.9 +    "overloaded" "pervasive" "private" "restricted" "shows"
   91.10 +    "structure" "unchecked" "where" "|"
   91.11    and "text" "txt" :: document_body
   91.12    and "text_raw" :: document_raw
   91.13    and "default_sort" :: thy_decl == ""
    92.1 --- a/src/Pure/Thy/thy_header.ML	Mon Apr 06 15:23:50 2015 +0200
    92.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Apr 06 23:24:45 2015 +0200
    92.3 @@ -6,7 +6,7 @@
    92.4  
    92.5  signature THY_HEADER =
    92.6  sig
    92.7 -  type keywords = (string * Keyword.spec option) list
    92.8 +  type keywords = ((string * Position.T) * Keyword.spec option) list
    92.9    type header =
   92.10     {name: string * Position.T,
   92.11      imports: (string * Position.T) list,
   92.12 @@ -29,7 +29,7 @@
   92.13  
   92.14  (* header *)
   92.15  
   92.16 -type keywords = (string * Keyword.spec option) list;
   92.17 +type keywords = ((string * Position.T) * Keyword.spec option) list;
   92.18  
   92.19  type header =
   92.20   {name: string * Position.T,
   92.21 @@ -59,26 +59,26 @@
   92.22  val bootstrap_keywords =
   92.23    Keyword.empty_keywords
   92.24    |> Keyword.add_keywords
   92.25 -    [("%", NONE),
   92.26 -     ("(", NONE),
   92.27 -     (")", NONE),
   92.28 -     (",", NONE),
   92.29 -     ("::", NONE),
   92.30 -     ("==", NONE),
   92.31 -     ("and", NONE),
   92.32 -     (beginN, NONE),
   92.33 -     (importsN, NONE),
   92.34 -     (keywordsN, NONE),
   92.35 -     (headerN, SOME ((Keyword.document_heading, []), [])),
   92.36 -     (chapterN, SOME ((Keyword.document_heading, []), [])),
   92.37 -     (sectionN, SOME ((Keyword.document_heading, []), [])),
   92.38 -     (subsectionN, SOME ((Keyword.document_heading, []), [])),
   92.39 -     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
   92.40 -     (textN, SOME ((Keyword.document_body, []), [])),
   92.41 -     (txtN, SOME ((Keyword.document_body, []), [])),
   92.42 -     (text_rawN, SOME ((Keyword.document_raw, []), [])),
   92.43 -     (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
   92.44 -     ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
   92.45 +    [(("%", @{here}), NONE),
   92.46 +     (("(", @{here}), NONE),
   92.47 +     ((")", @{here}), NONE),
   92.48 +     ((",", @{here}), NONE),
   92.49 +     (("::", @{here}), NONE),
   92.50 +     (("==", @{here}), NONE),
   92.51 +     (("and", @{here}), NONE),
   92.52 +     ((beginN, @{here}), NONE),
   92.53 +     ((importsN, @{here}), NONE),
   92.54 +     ((keywordsN, @{here}), NONE),
   92.55 +     ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
   92.56 +     ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
   92.57 +     ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
   92.58 +     ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
   92.59 +     ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
   92.60 +     ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
   92.61 +     ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
   92.62 +     ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
   92.63 +     ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
   92.64 +     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
   92.65  
   92.66  
   92.67  (* theory data *)
   92.68 @@ -119,7 +119,7 @@
   92.69    Parse.group (fn () => "outer syntax keyword completion") Parse.name;
   92.70  
   92.71  val keyword_decl =
   92.72 -  Scan.repeat1 Parse.string --
   92.73 +  Scan.repeat1 (Parse.position Parse.string) --
   92.74    Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
   92.75    Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
   92.76    >> (fn ((names, spec), _) => map (rpair spec) names);
    93.1 --- a/src/Pure/Thy/thy_output.ML	Mon Apr 06 15:23:50 2015 +0200
    93.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Apr 06 23:24:45 2015 +0200
    93.3 @@ -384,10 +384,10 @@
    93.4          in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    93.5  
    93.6      val command = Scan.peek (fn d =>
    93.7 -      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
    93.8 +      Scan.optional (Scan.one Token.is_command_modifier -- improper >> op ::) [] --
    93.9        Scan.one Token.is_command -- Scan.repeat tag
   93.10 -      >> (fn ((private, cmd), tags) =>
   93.11 -        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
   93.12 +      >> (fn ((cmd_mod, cmd), tags) =>
   93.13 +        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
   93.14            [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
   93.15              (Basic_Token cmd, (Latex.markup_false, d)))]));
   93.16  
    94.1 --- a/src/Pure/Tools/class_deps.ML	Mon Apr 06 15:23:50 2015 +0200
    94.2 +++ b/src/Pure/Tools/class_deps.ML	Mon Apr 06 23:24:45 2015 +0200
    94.3 @@ -46,7 +46,7 @@
    94.4    || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
    94.5  
    94.6  val _ =
    94.7 -  Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
    94.8 +  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
    94.9      ((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
   94.10        (Toplevel.unknown_theory o
   94.11         Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
    95.1 --- a/src/Pure/Tools/find_consts.ML	Mon Apr 06 15:23:50 2015 +0200
    95.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Apr 06 23:24:45 2015 +0200
    95.3 @@ -140,7 +140,7 @@
    95.4  
    95.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    95.6  
    95.7 -val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
    95.8 +val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
    95.9  
   95.10  in
   95.11  
   95.12 @@ -151,7 +151,7 @@
   95.13    |> #1;
   95.14  
   95.15  val _ =
   95.16 -  Outer_Syntax.command @{command_spec "find_consts"}
   95.17 +  Outer_Syntax.command @{command_keyword find_consts}
   95.18      "find constants by name / type patterns"
   95.19      (query >> (fn spec =>
   95.20        Toplevel.keep (fn st =>
    96.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Apr 06 15:23:50 2015 +0200
    96.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 06 23:24:45 2015 +0200
    96.3 @@ -524,7 +524,7 @@
    96.4  
    96.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    96.6  
    96.7 -val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
    96.8 +val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
    96.9  
   96.10  in
   96.11  
   96.12 @@ -535,7 +535,7 @@
   96.13    |> #1;
   96.14  
   96.15  val _ =
   96.16 -  Outer_Syntax.command @{command_spec "find_theorems"}
   96.17 +  Outer_Syntax.command @{command_keyword find_theorems}
   96.18      "find theorems meeting specified criteria"
   96.19      (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   96.20        Toplevel.keep (fn st =>
    97.1 --- a/src/Pure/Tools/named_theorems.ML	Mon Apr 06 15:23:50 2015 +0200
    97.2 +++ b/src/Pure/Tools/named_theorems.ML	Mon Apr 06 23:24:45 2015 +0200
    97.3 @@ -89,7 +89,7 @@
    97.4    in (name, lthy') end;
    97.5  
    97.6  val _ =
    97.7 -  Outer_Syntax.local_theory @{command_spec "named_theorems"}
    97.8 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
    97.9      "declare named collection of theorems"
   97.10      (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   97.11        fold (fn (b, descr) => snd o declare b descr));
    98.1 --- a/src/Pure/Tools/rail.ML	Mon Apr 06 15:23:50 2015 +0200
    98.2 +++ b/src/Pure/Tools/rail.ML	Mon Apr 06 23:24:45 2015 +0200
    98.3 @@ -363,8 +363,7 @@
    98.4  in
    98.5  
    98.6  val _ = Theory.setup
    98.7 -  (Thy_Output.antiquotation @{binding rail}
    98.8 -    (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
    98.9 +  (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
   98.10      (fn {state, context, ...} => output_rules state o read context));
   98.11  
   98.12  end;
    99.1 --- a/src/Pure/Tools/thm_deps.ML	Mon Apr 06 15:23:50 2015 +0200
    99.2 +++ b/src/Pure/Tools/thm_deps.ML	Mon Apr 06 23:24:45 2015 +0200
    99.3 @@ -44,7 +44,7 @@
    99.4    end;
    99.5  
    99.6  val _ =
    99.7 -  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
    99.8 +  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
    99.9      (Parse.xthms1 >> (fn args =>
   99.10        Toplevel.unknown_theory o Toplevel.keep (fn state =>
   99.11          thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
   99.12 @@ -101,7 +101,7 @@
   99.13    in rev thms' end;
   99.14  
   99.15  val _ =
   99.16 -  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
   99.17 +  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   99.18      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   99.19         Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
   99.20          Toplevel.keep (fn state =>
   100.1 --- a/src/Pure/sign.ML	Mon Apr 06 15:23:50 2015 +0200
   100.2 +++ b/src/Pure/sign.ML	Mon Apr 06 23:24:45 2015 +0200
   100.3 @@ -525,6 +525,8 @@
   100.4  
   100.5  val private_scope = map_naming o Name_Space.private_scope;
   100.6  val private = map_naming o Name_Space.private;
   100.7 +val restricted_scope = map_naming o Name_Space.restricted_scope;
   100.8 +val restricted = map_naming o Name_Space.restricted;
   100.9  val concealed = map_naming Name_Space.concealed;
  100.10  
  100.11  
   101.1 --- a/src/Pure/theory.ML	Mon Apr 06 15:23:50 2015 +0200
   101.2 +++ b/src/Pure/theory.ML	Mon Apr 06 23:24:45 2015 +0200
   101.3 @@ -14,6 +14,7 @@
   101.4    val merge: theory * theory -> theory
   101.5    val merge_list: theory list -> theory
   101.6    val setup: (theory -> theory) -> unit
   101.7 +  val local_setup: (Proof.context -> Proof.context) -> unit
   101.8    val get_markup: theory -> Markup.T
   101.9    val axiom_table: theory -> term Name_Space.table
  101.10    val axiom_space: theory -> Name_Space.T
  101.11 @@ -51,6 +52,7 @@
  101.12    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
  101.13  
  101.14  fun setup f = Context.>> (Context.map_theory f);
  101.15 +fun local_setup f = Context.>> (Context.map_proof f);
  101.16  
  101.17  
  101.18  
   102.1 --- a/src/Sequents/prover.ML	Mon Apr 06 15:23:50 2015 +0200
   102.2 +++ b/src/Sequents/prover.ML	Mon Apr 06 23:24:45 2015 +0200
   102.3 @@ -68,7 +68,7 @@
   102.4    end;
   102.5  
   102.6  val _ =
   102.7 -  Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
   102.8 +  Outer_Syntax.command @{command_keyword print_pack} "print pack of classical rules"
   102.9      (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
  102.10  
  102.11  
   103.1 --- a/src/Tools/Code/code_haskell.ML	Mon Apr 06 15:23:50 2015 +0200
   103.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Apr 06 23:24:45 2015 +0200
   103.3 @@ -516,7 +516,7 @@
   103.4    #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
   103.5  
   103.6  val _ =
   103.7 -  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
   103.8 +  Outer_Syntax.command @{command_keyword code_monad} "define code syntax for monads"
   103.9      (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
  103.10        Toplevel.theory (add_monad target raw_bind)));
  103.11  
   104.1 --- a/src/Tools/Code/code_preproc.ML	Mon Apr 06 15:23:50 2015 +0200
   104.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Apr 06 23:24:45 2015 +0200
   104.3 @@ -588,7 +588,7 @@
   104.4    end);
   104.5  
   104.6  val _ =
   104.7 -  Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
   104.8 +  Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
   104.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
  104.10  
  104.11  end; (*struct*)
   105.1 --- a/src/Tools/Code/code_runtime.ML	Mon Apr 06 15:23:50 2015 +0200
   105.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Apr 06 23:24:45 2015 +0200
   105.3 @@ -475,7 +475,7 @@
   105.4  in
   105.5  
   105.6  val _ =
   105.7 -  Outer_Syntax.command @{command_spec "code_reflect"}
   105.8 +  Outer_Syntax.command @{command_keyword code_reflect}
   105.9      "enrich runtime environment with generated code"
  105.10      (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
  105.11        ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
   106.1 --- a/src/Tools/Code/code_target.ML	Mon Apr 06 15:23:50 2015 +0200
   106.2 +++ b/src/Tools/Code/code_target.ML	Mon Apr 06 23:24:45 2015 +0200
   106.3 @@ -638,25 +638,25 @@
   106.4    :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
   106.5  
   106.6  val _ =
   106.7 -  Outer_Syntax.command @{command_spec "code_reserved"}
   106.8 +  Outer_Syntax.command @{command_keyword code_reserved}
   106.9      "declare words as reserved for target language"
  106.10      (Parse.name -- Scan.repeat1 Parse.name
  106.11        >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
  106.12  
  106.13  val _ =
  106.14 -  Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols"
  106.15 +  Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
  106.16      (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
  106.17        >> (Toplevel.theory o fold set_identifiers_cmd));
  106.18  
  106.19  val _ =
  106.20 -  Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
  106.21 +  Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
  106.22      (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
  106.23        Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
  106.24        (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
  106.25        >> (Toplevel.theory o fold set_printings_cmd));
  106.26  
  106.27  val _ =
  106.28 -  Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
  106.29 +  Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
  106.30      (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
  106.31  
  106.32  end; (*struct*)
   107.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 06 15:23:50 2015 +0200
   107.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 06 23:24:45 2015 +0200
   107.3 @@ -957,14 +957,14 @@
   107.4  in
   107.5  
   107.6  val _ =
   107.7 -  Outer_Syntax.command @{command_spec "code_thms"}
   107.8 +  Outer_Syntax.command @{command_keyword code_thms}
   107.9      "print system of code equations for code"
  107.10      (Scan.repeat1 Parse.term >> (fn cs =>
  107.11        Toplevel.unknown_context o
  107.12        Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
  107.13  
  107.14  val _ =
  107.15 -  Outer_Syntax.command @{command_spec "code_deps"}
  107.16 +  Outer_Syntax.command @{command_keyword code_deps}
  107.17      "visualize dependencies of code equations for code"
  107.18      (Scan.repeat1 Parse.term >> (fn cs =>
  107.19        Toplevel.unknown_context o
   108.1 --- a/src/Tools/adhoc_overloading.ML	Mon Apr 06 15:23:50 2015 +0200
   108.2 +++ b/src/Tools/adhoc_overloading.ML	Mon Apr 06 23:24:45 2015 +0200
   108.3 @@ -233,12 +233,12 @@
   108.4    end;
   108.5  
   108.6  val _ =
   108.7 -  Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
   108.8 +  Outer_Syntax.local_theory @{command_keyword adhoc_overloading}
   108.9      "add adhoc overloading for constants / fixed variables"
  108.10      (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
  108.11  
  108.12  val _ =
  108.13 -  Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
  108.14 +  Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading}
  108.15      "delete adhoc overloading for constants / fixed variables"
  108.16      (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
  108.17  
   109.1 --- a/src/Tools/induct.ML	Mon Apr 06 15:23:50 2015 +0200
   109.2 +++ b/src/Tools/induct.ML	Mon Apr 06 23:24:45 2015 +0200
   109.3 @@ -88,7 +88,7 @@
   109.4     (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   109.5      (string * typ) list list -> term option list -> thm list option ->
   109.6      thm list -> int -> cases_tactic) ->
   109.7 -   theory -> theory
   109.8 +   local_theory -> local_theory
   109.9  end;
  109.10  
  109.11  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
  109.12 @@ -162,7 +162,7 @@
  109.13  
  109.14  val rearrange_eqs_simproc =
  109.15    Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
  109.16 -    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
  109.17 +    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t));
  109.18  
  109.19  
  109.20  (* rotate k premises to the left by j, skipping over first j premises *)
  109.21 @@ -257,7 +257,7 @@
  109.22    end;
  109.23  
  109.24  val _ =
  109.25 -  Outer_Syntax.command @{command_spec "print_induct_rules"}
  109.26 +  Outer_Syntax.command @{command_keyword print_induct_rules}
  109.27      "print induction and cases rules"
  109.28      (Scan.succeed (Toplevel.unknown_context o
  109.29        Toplevel.keep (print_rules o Toplevel.context_of)));
  109.30 @@ -363,14 +363,14 @@
  109.31  in
  109.32  
  109.33  val _ =
  109.34 -  Theory.setup
  109.35 -   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
  109.36 +  Theory.local_setup
  109.37 +   (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del)
  109.38        "declaration of cases rule" #>
  109.39 -    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
  109.40 +    Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del)
  109.41        "declaration of induction rule" #>
  109.42 -    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
  109.43 +    Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
  109.44        "declaration of coinduction rule" #>
  109.45 -    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
  109.46 +    Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
  109.47        "declaration of rules for simplifying induction or cases rules");
  109.48  
  109.49  end;
  109.50 @@ -515,7 +515,7 @@
  109.51  
  109.52  (** induct method **)
  109.53  
  109.54 -val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
  109.55 +val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction};
  109.56  
  109.57  
  109.58  (* atomize *)
  109.59 @@ -549,7 +549,7 @@
  109.60    rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
  109.61    rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
  109.62    Goal.conjunction_tac THEN_ALL_NEW
  109.63 -  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
  109.64 +  (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt);
  109.65  
  109.66  
  109.67  (* prepare rule *)
  109.68 @@ -737,10 +737,10 @@
  109.69    SUBGOAL_CASES (fn (_, i, st) =>
  109.70      let
  109.71        val thy = Proof_Context.theory_of ctxt;
  109.72 -  
  109.73 +
  109.74        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  109.75        val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
  109.76 -  
  109.77 +
  109.78        fun inst_rule (concls, r) =
  109.79          (if null insts then `Rule_Cases.get r
  109.80           else (align_left "Rule has fewer conclusions than arguments given"
  109.81 @@ -749,7 +749,7 @@
  109.82            |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
  109.83          |> mod_cases thy
  109.84          |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
  109.85 -  
  109.86 +
  109.87        val ruleq =
  109.88          (case opt_rule of
  109.89            SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
  109.90 @@ -759,7 +759,7 @@
  109.91              |> map_filter (Rule_Cases.mutual_rule ctxt)
  109.92              |> tap (trace_rules ctxt inductN o map #2)
  109.93              |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  109.94 -  
  109.95 +
  109.96        fun rule_cases ctxt rule cases =
  109.97          let
  109.98            val rule' = Rule_Cases.internalize_params rule;
  109.99 @@ -910,18 +910,8 @@
 109.100  
 109.101  in
 109.102  
 109.103 -val _ =
 109.104 -  Theory.setup
 109.105 -    (Method.setup @{binding cases}
 109.106 -      (Scan.lift (Args.mode no_simpN) --
 109.107 -        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
 109.108 -        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
 109.109 -          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
 109.110 -            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
 109.111 -      "case analysis on types or predicates/sets");
 109.112 -
 109.113  fun gen_induct_setup binding tac =
 109.114 -  Method.setup binding
 109.115 +  Method.local_setup binding
 109.116      (Scan.lift (Args.mode no_simpN) --
 109.117        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
 109.118          (arbitrary -- taking -- Scan.option induct_rule)) >>
 109.119 @@ -929,11 +919,17 @@
 109.120          Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
 109.121      "induction on types or predicates/sets";
 109.122  
 109.123 -val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
 109.124 -
 109.125  val _ =
 109.126 -  Theory.setup
 109.127 -    (Method.setup @{binding coinduct}
 109.128 +  Theory.local_setup
 109.129 +    (Method.local_setup @{binding cases}
 109.130 +      (Scan.lift (Args.mode no_simpN) --
 109.131 +        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
 109.132 +        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
 109.133 +          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
 109.134 +            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
 109.135 +      "case analysis on types or predicates/sets" #>
 109.136 +    gen_induct_setup @{binding induct} induct_tac #>
 109.137 +     Method.local_setup @{binding coinduct}
 109.138        (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
 109.139          (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
 109.140            Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
   110.1 --- a/src/Tools/induction.ML	Mon Apr 06 15:23:50 2015 +0200
   110.2 +++ b/src/Tools/induction.ML	Mon Apr 06 23:24:45 2015 +0200
   110.3 @@ -1,6 +1,14 @@
   110.4 +(*  Title:      Tools/induction.ML
   110.5 +    Author:     Tobias Nipkow, TU Muenchen
   110.6 +
   110.7 +Alternative proof method "induction" that gives induction hypotheses the
   110.8 +name "IH".
   110.9 +*)
  110.10 +
  110.11  signature INDUCTION =
  110.12  sig
  110.13 -  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
  110.14 +  val induction_tac: Proof.context -> bool ->
  110.15 +    (binding option * (term * bool)) option list list ->
  110.16      (string * typ) list list -> term option list -> thm list option ->
  110.17      thm list -> int -> cases_tactic
  110.18  end
  110.19 @@ -11,13 +19,13 @@
  110.20  val ind_hypsN = "IH";
  110.21  
  110.22  fun preds_of t =
  110.23 - (case strip_comb t of
  110.24 +  (case strip_comb t of
  110.25      (p as Var _, _) => [p]
  110.26    | (p as Free _, _) => [p]
  110.27 -  | (_, ts) => flat(map preds_of ts))
  110.28 +  | (_, ts) => maps preds_of ts);
  110.29  
  110.30  fun name_hyps (arg as ((cases, consumes), th)) =
  110.31 -  if not(forall (null o #2 o #1) cases) then arg
  110.32 +  if not (forall (null o #2 o #1) cases) then arg
  110.33    else
  110.34      let
  110.35        val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
  110.36 @@ -25,18 +33,18 @@
  110.37        val ps = preds_of concl;
  110.38  
  110.39        fun hname_of t =
  110.40 -        if exists_subterm (member (op =) ps) t
  110.41 -        then ind_hypsN else Rule_Cases.case_hypsN
  110.42 +        if exists_subterm (member (op aconv) ps) t
  110.43 +        then ind_hypsN else Rule_Cases.case_hypsN;
  110.44  
  110.45 -      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
  110.46 -      val n = Int.min (length hnamess, length cases) 
  110.47 -      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
  110.48 -        (take n cases ~~ take n hnamess)
  110.49 -    in ((cases',consumes),th) end
  110.50 +      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
  110.51 +      val n = Int.min (length hnamess, length cases);
  110.52 +      val cases' =
  110.53 +        map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
  110.54 +          (take n cases ~~ take n hnamess);
  110.55 +    in ((cases', consumes), th) end;
  110.56  
  110.57 -val induction_tac = Induct.gen_induct_tac (K name_hyps)
  110.58 +val induction_tac = Induct.gen_induct_tac (K name_hyps);
  110.59  
  110.60 -val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
  110.61 +val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
  110.62  
  110.63  end
  110.64 -
   111.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Apr 06 15:23:50 2015 +0200
   111.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Apr 06 23:24:45 2015 +0200
   111.3 @@ -39,10 +39,18 @@
   111.4      protected var _end = int_to_pos(range.stop)
   111.5      override def getIcon: Icon = null
   111.6      override def getShortString: String =
   111.7 -      "<html><span style=\"" + css + "\">" +
   111.8 -      (if (keyword != "" && _name.startsWith(keyword))
   111.9 -        "<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
  111.10 -       else HTML.encode(_name)) + "</span></html>"
  111.11 +    {
  111.12 +      val n = keyword.length
  111.13 +      val s =
  111.14 +        _name.indexOf(keyword) match {
  111.15 +          case i if i >= 0 && n > 0 =>
  111.16 +            HTML.encode(_name.substring(0, i)) +
  111.17 +            "<b>" + HTML.encode(keyword) + "</b>" +
  111.18 +            HTML.encode(_name.substring(i + n))
  111.19 +          case _ => HTML.encode(_name)
  111.20 +        }
  111.21 +      "<html><span style=\"" + css + "\">" + s + "</span></html>"
  111.22 +    }
  111.23      override def getLongString: String = _name
  111.24      override def getName: String = _name
  111.25      override def setName(name: String) = _name = name
   112.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 15:23:50 2015 +0200
   112.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 23:24:45 2015 +0200
   112.3 @@ -274,11 +274,11 @@
   112.4    {
   112.5      def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
   112.6        token_reverse_iterator(syntax, buffer, i).
   112.7 -        find(info => info.info.is_private || info.info.is_command)
   112.8 +        find(info => info.info.is_command_modifier || info.info.is_command)
   112.9  
  112.10      def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
  112.11        token_iterator(syntax, buffer, i).
  112.12 -        find(info => info.info.is_private || info.info.is_command)
  112.13 +        find(info => info.info.is_command_modifier || info.info.is_command)
  112.14  
  112.15      if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
  112.16        val start_info =
  112.17 @@ -288,15 +288,15 @@
  112.18            case Some(Text.Info(range1, tok1)) if tok1.is_command =>
  112.19              val info2 = maybe_command_start(range1.start - 1)
  112.20              info2 match {
  112.21 -              case Some(Text.Info(_, tok2)) if tok2.is_private => info2
  112.22 +              case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
  112.23                case _ => info1
  112.24              }
  112.25            case _ => info1
  112.26          }
  112.27        }
  112.28 -      val (start_is_private, start, start_next) =
  112.29 +      val (start_is_command_modifier, start, start_next) =
  112.30          start_info match {
  112.31 -          case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop)
  112.32 +          case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
  112.33            case None => (false, 0, 0)
  112.34          }
  112.35  
  112.36 @@ -304,7 +304,7 @@
  112.37        {
  112.38          val info1 = maybe_command_stop(start_next)
  112.39          info1 match {
  112.40 -          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private =>
  112.41 +          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
  112.42              maybe_command_stop(range1.stop)
  112.43            case _ => info1
  112.44          }
   113.1 --- a/src/Tools/permanent_interpretation.ML	Mon Apr 06 15:23:50 2015 +0200
   113.2 +++ b/src/Tools/permanent_interpretation.ML	Mon Apr 06 23:24:45 2015 +0200
   113.3 @@ -95,7 +95,7 @@
   113.4  end;
   113.5  
   113.6  val _ =
   113.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
   113.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
   113.9      "prove interpretation of locale expression into named theory"
  113.10      (Parse.!!! (Parse_Spec.locale_expression true) --
  113.11        Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   114.1 --- a/src/Tools/quickcheck.ML	Mon Apr 06 15:23:50 2015 +0200
   114.2 +++ b/src/Tools/quickcheck.ML	Mon Apr 06 23:24:45 2015 +0200
   114.3 @@ -527,11 +527,11 @@
   114.4    @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
   114.5  
   114.6  val _ =
   114.7 -  Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
   114.8 +  Outer_Syntax.command @{command_keyword quickcheck_params} "set parameters for random testing"
   114.9      (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
  114.10  
  114.11  val _ =
  114.12 -  Outer_Syntax.command @{command_spec "quickcheck"}
  114.13 +  Outer_Syntax.command @{command_keyword quickcheck}
  114.14      "try to find counterexample for subgoal"
  114.15      (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
  114.16        Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
   115.1 --- a/src/Tools/solve_direct.ML	Mon Apr 06 15:23:50 2015 +0200
   115.2 +++ b/src/Tools/solve_direct.ML	Mon Apr 06 23:24:45 2015 +0200
   115.3 @@ -92,7 +92,7 @@
   115.4  val solve_direct = do_solve_direct Normal
   115.5  
   115.6  val _ =
   115.7 -  Outer_Syntax.command @{command_spec "solve_direct"}
   115.8 +  Outer_Syntax.command @{command_keyword solve_direct}
   115.9      "try to solve conjectures directly with existing theorems"
  115.10      (Scan.succeed (Toplevel.unknown_proof o
  115.11        Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
   116.1 --- a/src/Tools/subtyping.ML	Mon Apr 06 15:23:50 2015 +0200
   116.2 +++ b/src/Tools/subtyping.ML	Mon Apr 06 23:24:45 2015 +0200
   116.3 @@ -1115,7 +1115,7 @@
   116.4  (* outer syntax commands *)
   116.5  
   116.6  val _ =
   116.7 -  Outer_Syntax.command @{command_spec "print_coercions"}
   116.8 +  Outer_Syntax.command @{command_keyword print_coercions}
   116.9      "print information about coercions"
  116.10      (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
  116.11  
   117.1 --- a/src/Tools/try.ML	Mon Apr 06 15:23:50 2015 +0200
   117.2 +++ b/src/Tools/try.ML	Mon Apr 06 23:24:45 2015 +0200
   117.3 @@ -75,7 +75,7 @@
   117.4      |> tap (fn NONE => writeln "Tried in vain." | _ => ())
   117.5  
   117.6  val _ =
   117.7 -  Outer_Syntax.command @{command_spec "try"}
   117.8 +  Outer_Syntax.command @{command_keyword try}
   117.9      "try a combination of automatic proving and disproving tools"
  117.10      (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
  117.11  
   118.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Apr 06 15:23:50 2015 +0200
   118.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Apr 06 23:24:45 2015 +0200
   118.3 @@ -430,7 +430,7 @@
   118.4  
   118.5  val _ =
   118.6    Outer_Syntax.command
   118.7 -    (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
   118.8 +    (if coind then @{command_keyword codatatype} else @{command_keyword datatype})
   118.9      ("define " ^ coind_prefix ^ "datatype")
  118.10      ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
  118.11        Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
   119.1 --- a/src/ZF/Tools/ind_cases.ML	Mon Apr 06 15:23:50 2015 +0200
   119.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon Apr 06 23:24:45 2015 +0200
   119.3 @@ -53,7 +53,7 @@
   119.4    in thy |> Global_Theory.note_thmss "" facts |> snd end;
   119.5  
   119.6  val _ =
   119.7 -  Outer_Syntax.command @{command_spec "inductive_cases"}
   119.8 +  Outer_Syntax.command @{command_keyword inductive_cases}
   119.9      "create simplified instances of elimination rules (improper)"
  119.10      (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
  119.11        >> (Toplevel.theory o inductive_cases));
   120.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Apr 06 15:23:50 2015 +0200
   120.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Apr 06 23:24:45 2015 +0200
   120.3 @@ -191,7 +191,7 @@
   120.4  (* outer syntax *)
   120.5  
   120.6  val _ =
   120.7 -  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
   120.8 +  Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
   120.9      ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
  120.10       (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
  120.11       (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
   121.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Apr 06 15:23:50 2015 +0200
   121.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Apr 06 23:24:45 2015 +0200
   121.3 @@ -595,7 +595,7 @@
   121.4  
   121.5  val _ =
   121.6    Outer_Syntax.command
   121.7 -    (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
   121.8 +    (if coind then @{command_keyword coinductive} else @{command_keyword inductive})
   121.9      ("define " ^ co_prefix ^ "inductive sets") ind_decl;
  121.10  
  121.11  end;
   122.1 --- a/src/ZF/Tools/primrec_package.ML	Mon Apr 06 15:23:50 2015 +0200
   122.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon Apr 06 23:24:45 2015 +0200
   122.3 @@ -197,7 +197,7 @@
   122.4  (* outer syntax *)
   122.5  
   122.6  val _ =
   122.7 -  Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
   122.8 +  Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
   122.9      (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
  122.10        >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
  122.11  
   123.1 --- a/src/ZF/Tools/typechk.ML	Mon Apr 06 15:23:50 2015 +0200
   123.2 +++ b/src/ZF/Tools/typechk.ML	Mon Apr 06 23:24:45 2015 +0200
   123.3 @@ -126,7 +126,7 @@
   123.4        "ZF type-checking");
   123.5  
   123.6  val _ =
   123.7 -  Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
   123.8 +  Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
   123.9      (Scan.succeed (Toplevel.unknown_context o
  123.10        Toplevel.keep (print_tcset o Toplevel.context_of)));
  123.11