# HG changeset patch
# User wenzelm
# Date 1390684700 -3600
# Node ID de95c97efab348673e0ee28d09cab10cef2e0fb5
# Parent  ee5a0ca00b6f6dce95a63b68ffe1770a5f3fb4fe# Parent  04448228381de3b493d3a47a0b57bc48d5d8fb9f
merged

diff -r ee5a0ca00b6f -r de95c97efab3 .hgignore
--- a/.hgignore	Sat Jan 25 19:07:07 2014 +0100
+++ b/.hgignore	Sat Jan 25 22:18:20 2014 +0100
@@ -5,7 +5,6 @@
 *.jar
 *.orig
 *.rej
-*.pyc
 .DS_Store
 .swp
 
diff -r ee5a0ca00b6f -r de95c97efab3 Admin/user-aliases
--- a/Admin/user-aliases	Sat Jan 25 19:07:07 2014 +0100
+++ b/Admin/user-aliases	Sat Jan 25 22:18:20 2014 +0100
@@ -1,4 +1,5 @@
 lcp paulson
+lp15@cam.ac.uk paulson
 norbert.schirmer@web.de schirmer
 schirmer@in.tum.de schirmer
 urbanc@in.tum.de urbanc
diff -r ee5a0ca00b6f -r de95c97efab3 NEWS
--- a/NEWS	Sat Jan 25 19:07:07 2014 +0100
+++ b/NEWS	Sat Jan 25 22:18:20 2014 +0100
@@ -40,6 +40,10 @@
 
 *** Pure ***
 
+* Attributes "where" and "of" allow an optional context of local
+variables ('for' declaration): these variables become schematic in the
+instantiated theorem.
+
 * More thorough check of proof context for goal statements and
 attributed fact expressions (concerning background theory, declared
 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
@@ -53,6 +57,9 @@
 
 *** HOL ***
 
+* Simproc "finite_Collect" is no longer enabled by default, due to
+spurious crashes and other surprises.  Potential INCOMPATIBILITY.
+
 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
   "primrec_new", "primcorec", and "primcorecursive" command are now part of
@@ -266,6 +273,13 @@
 
 *** ML ***
 
+* Proper context discipline for read_instantiate and instantiate_tac:
+variables that are meant to become schematic need to be given as
+fixed, and are generalized by the explicit context of local variables.
+This corresponds to Isar attributes "where" and "of" with 'for'
+declaration.  INCOMPATIBILITY, also due to potential change of indices
+of schematic variables.
+
 * Toplevel function "use" refers to raw ML bootstrap environment,
 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
 Note that 'ML_file' is the canonical command to load ML files into the
diff -r ee5a0ca00b6f -r de95c97efab3 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -721,11 +721,13 @@
     ;
     @@{attribute OF} @{syntax thmrefs}
     ;
-    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
+    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
+      (@'for' (@{syntax vars} + @'and'))?
     ;
     @@{attribute "where"}
       ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
-      (@{syntax type} | @{syntax term}) * @'and')
+      (@{syntax type} | @{syntax term}) * @'and') \<newline>
+      (@'for' (@{syntax vars} + @'and'))?
   \<close>}
 
   \begin{description}
@@ -812,6 +814,10 @@
   left to right; ``@{text _}'' (underscore) indicates to skip a
   position.  Arguments following a ``@{text "concl:"}'' specification
   refer to positions of the conclusion of a rule.
+
+  An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+  be specified: the instantiated theorem is exported, and these
+  variables become schematic (usually with some shifting of indices).
   
   \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
   performs named instantiation of schematic type and term variables
@@ -821,6 +827,9 @@
   As type instantiations are inferred from term instantiations,
   explicit type instantiations are seldom necessary.
 
+  An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+  be specified as for @{attribute "of"} above.
+
   \end{description}
 *}
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -93,7 +93,7 @@
 (*Simplifying   
  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
   This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -256,7 +256,7 @@
        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
 
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
 
 ML
 {*
@@ -290,7 +290,7 @@
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
 
 ML
 {*
diff -r ee5a0ca00b6f -r de95c97efab3 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -190,7 +190,7 @@
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
@@ -388,9 +388,9 @@
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -404,7 +404,7 @@
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties *}
 
@@ -786,21 +786,23 @@
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
 
-lemmas pushKeys [standard] =
+lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
+  for K C N X Y K'
 
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
+  for X K C N X' Y
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered. *}
diff -r ee5a0ca00b6f -r de95c97efab3 src/Doc/isar.sty
--- a/src/Doc/isar.sty	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/isar.sty	Sat Jan 25 22:18:20 2014 +0100
@@ -11,6 +11,7 @@
 \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
 
+\newcommand{\isasymFOR}{\isakeyword{for}}
 \newcommand{\isasymAND}{\isakeyword{and}}
 \newcommand{\isasymIS}{\isakeyword{is}}
 \newcommand{\isasymWHERE}{\isakeyword{where}}
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -41,9 +41,9 @@
 declare lvar_def [simp]
 
 ML {*
-fun inst1_tac ctxt s t st =
+fun inst1_tac ctxt s t xs st =
   case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
-  SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
+  SOME i => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty;
 
 val ax_tac =
   REPEAT o rtac allI THEN'
@@ -64,7 +64,7 @@
 apply  (tactic "ax_tac 1" (* Try *))
 defer
 apply    (tactic {* inst1_tac @{context} "Q" 
-                 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
+                 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
 prefer 2
 apply    simp
 apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
@@ -83,7 +83,7 @@
 apply   (tactic "ax_tac 1" (* AVar *))
 prefer 2
 apply    (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
 apply    (simp del: avar_def2 peek_and_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -124,7 +124,7 @@
 apply      (tactic "ax_tac 1") (* Ass *)
 prefer 2
 apply       (rule ax_subst_Var_allI)
-apply       (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply       (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *})
 apply       (rule allI)
 apply       (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
 apply       (rule ax_derivs.Abrupt)
@@ -132,17 +132,17 @@
 apply      (tactic "ax_tac 1" (* FVar *))
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")
-apply     (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
+apply     (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" [] *})
 apply     fastforce
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
-apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
 apply   (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
 apply   (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *})
 apply    (simp del: peek_and_def2 heap_free_def2 normal_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -161,7 +161,7 @@
 apply (tactic "ax_tac 1")
 defer
 apply  (rule ax_subst_Var_allI)
-apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
+apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
 apply  (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
@@ -189,18 +189,18 @@
 apply     (tactic "ax_tac 1")
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
-apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *})
 apply     (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
 apply      (tactic "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac 3")
-apply      (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
+apply      (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *})
 apply      (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
 apply      (tactic "ax_tac 2")
 apply     (tactic "ax_tac 1" (* FVar *))
 apply      (tactic "ax_tac 2" (* StatRef *))
 apply     (rule ax_derivs.Done [THEN conseq1])
-apply     (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
+apply     (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" [] *})
 apply     (clarsimp split del: split_if)
 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
 apply     (drule initedD)
@@ -210,9 +210,9 @@
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp
-apply   (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+apply   (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *})
 apply   clarsimp
-apply  (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
+apply  (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *})
 apply  clarsimp
      (* end init *)
 apply (rule conseq1)
@@ -244,7 +244,7 @@
 apply  clarsimp
 apply (tactic "ax_tac 1" (* If *))
 apply  (tactic 
-  {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+  {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *})
 apply  (tactic "ax_tac 1")
 apply  (rule conseq1)
 apply   (tactic "ax_tac 1")
@@ -265,7 +265,7 @@
 apply  (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Var_allI)
-apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
 apply   (rule allI)
 apply   (rule_tac P' = "Normal ?P" in conseq1)
 prefer 2
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Bali/Basis.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -181,7 +181,7 @@
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
   simplify (ctxt delsimps [@{thm not_None_eq}])
-    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"]
 *}
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Library/Binomial.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -131,7 +131,7 @@
          prefer 4 apply (force simp add: constr_bij)
         prefer 3 apply force
        prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
-         finite_subset [of _ "Pow (insert x F)", standard])
+         finite_subset [of _ "Pow (insert x F)" for F])
       apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
       done
   qed
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -284,8 +284,8 @@
 lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
 
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
 
 subsection {* Order instances *}
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -1514,8 +1514,7 @@
     assume i: "i \<in> Basis"
     have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
       norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
-      by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf uminus_add_conv_diff
-            norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
+      by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
     also have "\<dots> \<le> e + e"
       unfolding real_norm_def
       by (intro add_mono norm_bound_Basis_le i fPs) auto
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -133,7 +133,7 @@
          prefer 4 apply (force simp add: constr_bij)
         prefer 3 apply force
        prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
-         finite_subset [of _ "Pow (insert x F)", standard])
+         finite_subset [of _ "Pow (insert x F)" for F])
       apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
       done
   qed
@@ -669,7 +669,9 @@
     have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
       using assms by(auto intro!: inj_onI)
     moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
-      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq]  dest: finite_subset intro: card_mono)
+      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
+        simp add: card_gt_0_iff[folded Suc_le_eq]
+        dest: finite_subset intro: card_mono)
     ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
       by(rule setsum_reindex_cong[where f=snd]) fastforce
     also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Prolog/prolog.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -49,14 +49,16 @@
 fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
                         then thm else raise not_HOHH);
 
-fun atomizeD ctxt thm = let
+fun atomizeD ctxt thm =
+  let
     fun at  thm = case concl_of thm of
-      _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
-        (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
+      _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
+        let val s' = if s="P" then "PP" else s
+        in at(thm RS (read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end
     | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
     | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
     | _                             => [thm]
-in map zero_var_indexes (at thm) end;
+  in map zero_var_indexes (at thm) end;
 
 val atomize_ss =
   (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs))
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Rat.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -622,8 +622,8 @@
     (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
       @{thm True_implies_equals},
-      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
-      read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
+      @{thm distrib_left [where a = "numeral v" for v]},
+      @{thm distrib_left [where a = "- numeral v" for v]},
       @{thm divide_1}, @{thm divide_zero_left},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Set.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -1577,10 +1577,10 @@
   by (auto simp add: Pow_def)
 
 lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
-  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
+  by (blast intro: image_eqI [where ?x = "u - {a}" for u])
 
 lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
-  by (blast intro: exI [where ?x = "- u", standard])
+  by (blast intro: exI [where ?x = "- u" for u])
 
 lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
   by blast
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -728,7 +728,7 @@
 qed auto
 
 lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
-by(auto intro!: image_eqI[where x="nat x", standard])
+  by (auto intro!: image_eqI [where x = "nat x" for x])
 
 context ordered_ab_group_add
 begin
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -416,7 +416,7 @@
                  |> hackish_string_of_term ctxt
   in
     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
-      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
+      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)] [])
   end
 
 fun type_match thy (T1, T2) =
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -130,7 +130,7 @@
   rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
-val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
+val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
 
 fun tracing true _ = ()
   | tracing false msg = writeln msg;
diff -r ee5a0ca00b6f -r de95c97efab3 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -52,35 +52,35 @@
   end;
 *}
 
-syntax "_STR_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
+syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string"  ("_")
 
 parse_translation {*
-  [(@{syntax_const "_STR_cartouche"},
+  [(@{syntax_const "_cartouche_string"},
     K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
 *}
 
-term "STR \<open>\<close>"
-term "STR \<open>abc\<close>"
-term "STR \<open>abc\<close> @ STR \<open>xyz\<close>"
-term "STR \<open>\<newline>\<close>"
-term "STR \<open>\001\010\100\<close>"
+term "\<open>\<close>"
+term "\<open>abc\<close>"
+term "\<open>abc\<close> @ \<open>xyz\<close>"
+term "\<open>\<newline>\<close>"
+term "\<open>\001\010\100\<close>"
 
 
 subsection {* Alternate outer and inner syntax: string literals *}
 
 subsubsection {* Nested quotes *}
 
-syntax "_STR_string" :: "string_position \<Rightarrow> string"  ("STR _")
+syntax "_string_string" :: "string_position \<Rightarrow> string"  ("_")
 
 parse_translation {*
-  [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))]
+  [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
 *}
 
-term "STR \"\""
-term "STR \"abc\""
-term "STR \"abc\" @ STR \"xyz\""
-term "STR \"\<newline>\""
-term "STR \"\001\010\100\""
+term "\"\""
+term "\"abc\""
+term "\"abc\" @ \"xyz\""
+term "\"\<newline>\""
+term "\"\001\010\100\""
 
 
 subsubsection {* Term cartouche and regular quotes *}
@@ -95,11 +95,11 @@
         in writeln (Syntax.string_of_term ctxt t) end)))
 *}
 
-term_cartouche \<open>STR ""\<close>
-term_cartouche \<open>STR "abc"\<close>
-term_cartouche \<open>STR "abc" @ STR "xyz"\<close>
-term_cartouche \<open>STR "\<newline>"\<close>
-term_cartouche \<open>STR "\001\010\100"\<close>
+term_cartouche \<open>""\<close>
+term_cartouche \<open>"abc"\<close>
+term_cartouche \<open>"abc" @ "xyz"\<close>
+term_cartouche \<open>"\<newline>"\<close>
+term_cartouche \<open>"\001\010\100"\<close>
 
 
 subsubsection {* Further nesting: antiquotations *}
@@ -125,22 +125,22 @@
 *}
 
 ML {*
-  @{term_cartouche \<open>STR ""\<close>};
-  @{term_cartouche \<open>STR "abc"\<close>};
-  @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
-  @{term_cartouche \<open>STR "\<newline>"\<close>};
-  @{term_cartouche \<open>STR "\001\010\100"\<close>};
+  @{term_cartouche \<open>""\<close>};
+  @{term_cartouche \<open>"abc"\<close>};
+  @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+  @{term_cartouche \<open>"\<newline>"\<close>};
+  @{term_cartouche \<open>"\001\010\100"\<close>};
 *}
 
 text {*
   @{ML_cartouche
     \<open>
       (
-        @{term_cartouche \<open>STR ""\<close>};
-        @{term_cartouche \<open>STR "abc"\<close>};
-        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
-        @{term_cartouche \<open>STR "\<newline>"\<close>};
-        @{term_cartouche \<open>STR "\001\010\100"\<close>}
+        @{term_cartouche \<open>""\<close>};
+        @{term_cartouche \<open>"abc"\<close>};
+        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+        @{term_cartouche \<open>"\<newline>"\<close>};
+        @{term_cartouche \<open>"\001\010\100"\<close>}
       )
     \<close>
   }
@@ -160,11 +160,11 @@
   @{ML_cartouche
     \<open>
       (
-        @{term_cartouche \<open>STR ""\<close>};
-        @{term_cartouche \<open>STR "abc"\<close>};
-        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
-        @{term_cartouche \<open>STR "\<newline>"\<close>};
-        @{term_cartouche \<open>STR "\001\010\100"\<close>}
+        @{term_cartouche \<open>""\<close>};
+        @{term_cartouche \<open>"abc"\<close>};
+        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+        @{term_cartouche \<open>"\<newline>"\<close>};
+        @{term_cartouche \<open>"\001\010\100"\<close>}
       )
     \<close>
   }
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -37,6 +37,7 @@
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     theory -> theory
+  val internal: (morphism -> attribute) -> src
   val add_del: attribute -> attribute -> attribute context_parser
   val thm_sel: Facts.interval list parser
   val thm: thm context_parser
@@ -45,7 +46,6 @@
   val partial_evaluation: Proof.context ->
     (binding * (thm list * Args.src list) list) list ->
     (binding * (thm list * Args.src list) list) list
-  val internal: (morphism -> attribute) -> src
   val print_options: Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -194,6 +194,15 @@
       ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
 
 
+(* internal attribute *)
+
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
+
+val _ = Theory.setup
+ (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+    "internal attribute");
+
+
 (* add/del syntax *)
 
 fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
@@ -318,119 +327,6 @@
 
 
 
-(** basic attributes **)
-
-(* internal *)
-
-fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
-
-
-(* rule composition *)
-
-val THEN_att =
-  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
-    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
-
-val OF_att =
-  thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
-
-
-(* rename_abs *)
-
-val rename_abs =
-  Scan.repeat (Args.maybe Args.name)
-  >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
-
-
-(* unfold / fold definitions *)
-
-fun unfolded_syntax rule =
-  thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
-
-val unfolded = unfolded_syntax Local_Defs.unfold;
-val folded = unfolded_syntax Local_Defs.fold;
-
-
-(* rule format *)
-
-fun rule_format true = Object_Logic.rule_format_no_asm
-  | rule_format false = Object_Logic.rule_format;
-
-val elim_format = Thm.rule_attribute (K Tactic.make_elim);
-
-
-(* case names *)
-
-val case_names =
-  Scan.repeat1 (Args.name --
-    Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
-  (fn cs =>
-    Rule_Cases.cases_hyp_names (map fst cs)
-      (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
-
-
-(* misc rules *)
-
-val no_vars = Thm.rule_attribute (fn context => fn th =>
-  let
-    val ctxt = Variable.set_body false (Context.proof_of context);
-    val ((_, [th']), _) = Variable.import true [th] ctxt;
-  in th' end);
-
-val eta_long =
-  Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
-
-val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
-
-
-(* theory setup *)
-
-val _ = Theory.setup
- (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
-    "internal attribute" #>
-  setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
-  setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
-  setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
-  setup (Binding.name "THEN") THEN_att "resolution with rule" #>
-  setup (Binding.name "OF") OF_att "rule applied to facts" #>
-  setup (Binding.name "rename_abs") (Scan.lift rename_abs)
-    "rename bound variables in abstractions" #>
-  setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
-  setup (Binding.name "folded") folded "folded definitions" #>
-  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
-    "number of consumed facts" #>
-  setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
-    "number of equality constraints" #>
-  setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
-  setup (Binding.name "case_conclusion")
-    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
-    "named conclusion of rule cases" #>
-  setup (Binding.name "params")
-    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
-    "named rule parameters" #>
-  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
-    "result put into standard form (legacy)" #>
-  setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
-    "result put into canonical rule format" #>
-  setup (Binding.name "elim_format") (Scan.succeed elim_format)
-    "destruct rule turned into elimination rule format" #>
-  setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
-  setup (Binding.name "eta_long") (Scan.succeed eta_long)
-    "put theorem into eta long beta normal form" #>
-  setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
-    "declaration of atomize rule" #>
-  setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
-    "declaration of rulify rule" #>
-  setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
-  setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
-    "declaration of definitional transformations" #>
-  setup (Binding.name "abs_def")
-    (Scan.succeed (Thm.rule_attribute (fn context =>
-      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
-    "abstract over free variables of definitional theorem");
-
-
-
 (** configuration options **)
 
 (* naming *)
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -95,11 +95,11 @@
 (* concrete syntax *)
 
 val _ = Theory.setup
- (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
     "declaration of transitivity rule" #>
-  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+  Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
     "declaration of symmetry rule" #>
-  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+  Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
     "resolution with symmetry rule" #>
   Global_Theory.add_thms
    [((Binding.empty, transitive_thm), [trans_add]),
@@ -197,4 +197,32 @@
 val moreover = collect false;
 val ultimately = collect true;
 
+
+(* outer syntax *)
+
+val calc_args =
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
+
+val _ =
+  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+    (calc_args >> (Toplevel.proofs' o also_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_spec "finally"}
+    "combine calculation and current facts, exhibit result"
+    (calc_args >> (Toplevel.proofs' o finally_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+    (Scan.succeed (Toplevel.proof' moreover));
+
+val _ =
+  Outer_Syntax.command @{command_spec "ultimately"}
+    "augment calculation by current facts, exhibit result"
+    (Scan.succeed (Toplevel.proof' ultimately));
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+
 end;
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -688,30 +688,6 @@
       Toplevel.skip_proof (fn i => i + 1)));
 
 
-(* calculational proof commands *)
-
-val calc_args =
-  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
-
-val _ =
-  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
-    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_spec "finally"}
-    "combine calculation and current facts, exhibit result"
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
-    (Scan.succeed (Toplevel.proof' Calculation.moreover));
-
-val _ =
-  Outer_Syntax.command @{command_spec "ultimately"}
-    "augment calculation by current facts, exhibit result"
-    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
-
-
 (* proof navigation *)
 
 val _ =
@@ -847,11 +823,6 @@
       Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/token.scala	Sat Jan 25 22:18:20 2014 +0100
@@ -108,7 +108,7 @@
     else source
 
   def text: (String, String) =
-    if (is_command && source == ";") ("terminator", "")
+    if (is_keyword && source == ";") ("terminator", "")
     else (kind.toString, source)
 }
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Pure.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -103,6 +103,7 @@
 begin
 
 ML_file "Isar/isar_syn.ML"
+ML_file "Isar/calculation.ML"
 ML_file "Tools/rail.ML"
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/find_theorems.ML"
@@ -111,6 +112,117 @@
 ML_file "Tools/simplifier_trace.ML"
 
 
+section {* Basic attributes *}
+
+attribute_setup tagged =
+  "Scan.lift (Args.name -- Args.name) >> Thm.tag"
+  "tagged theorem"
+
+attribute_setup untagged =
+  "Scan.lift Args.name >> Thm.untag"
+  "untagged theorem"
+
+attribute_setup kind =
+  "Scan.lift Args.name >> Thm.kind"
+  "theorem kind"
+
+attribute_setup THEN =
+  "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
+    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
+  "resolution with rule"
+
+attribute_setup OF =
+  "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
+  "rule resolved with facts"
+
+attribute_setup rename_abs =
+  "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
+    Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
+  "rename bound variables in abstractions"
+
+attribute_setup unfolded =
+  "Attrib.thms >> (fn ths =>
+    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
+  "unfolded definitions"
+
+attribute_setup folded =
+  "Attrib.thms >> (fn ths =>
+    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
+  "folded definitions"
+
+attribute_setup consumes =
+  "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
+  "number of consumed facts"
+
+attribute_setup constraints =
+  "Scan.lift Parse.nat >> Rule_Cases.constraints"
+  "number of equality constraints"
+
+attribute_setup case_names = {*
+  Scan.lift (Scan.repeat1 (Args.name --
+    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
+  >> (fn cs =>
+      Rule_Cases.cases_hyp_names
+        (map #1 cs)
+        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
+*} "named rule cases"
+
+attribute_setup case_conclusion =
+  "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
+  "named conclusion of rule cases"
+
+attribute_setup params =
+  "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
+  "named rule parameters"
+
+attribute_setup standard =
+  "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
+  "result put into standard form (legacy)"
+
+attribute_setup rule_format = {*
+  Scan.lift (Args.mode "no_asm")
+    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
+*} "result put into canonical rule format"
+
+attribute_setup elim_format =
+  "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
+  "destruct rule turned into elimination rule format"
+
+attribute_setup no_vars = {*
+  Scan.succeed (Thm.rule_attribute (fn context => fn th =>
+    let
+      val ctxt = Variable.set_body false (Context.proof_of context);
+      val ((_, [th']), _) = Variable.import true [th] ctxt;
+    in th' end))
+*} "imported schematic variables"
+
+attribute_setup eta_long =
+  "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
+  "put theorem into eta long beta normal form"
+
+attribute_setup atomize =
+  "Scan.succeed Object_Logic.declare_atomize"
+  "declaration of atomize rule"
+
+attribute_setup rulify =
+  "Scan.succeed Object_Logic.declare_rulify"
+  "declaration of rulify rule"
+
+attribute_setup rotated =
+  "Scan.lift (Scan.optional Parse.int 1
+    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
+  "rotated theorem premises"
+
+attribute_setup defn =
+  "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
+  "declaration of definitional transformations"
+
+attribute_setup abs_def =
+  "Scan.succeed (Thm.rule_attribute (fn context =>
+    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
+  "abstract over free variables of definitional theorem"
+
+
 section {* Further content for the Pure theory *}
 
 subsection {* Meta-level connectives in assumptions *}
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/ROOT	Sat Jan 25 22:18:20 2014 +0100
@@ -106,7 +106,6 @@
     "Isar/attrib.ML"
     "Isar/auto_bind.ML"
     "Isar/bundle.ML"
-    "Isar/calculation.ML"
     "Isar/class.ML"
     "Isar/class_declaration.ML"
     "Isar/code.ML"
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/ROOT.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -236,9 +236,6 @@
 use "Isar/method.ML";
 use "Isar/proof.ML";
 use "Isar/element.ML";
-
-(*derived theory and proof elements*)
-use "Isar/calculation.ML";
 use "Isar/obtain.ML";
 
 (*local theories and targets*)
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/System/session.scala	Sat Jan 25 22:18:20 2014 +0100
@@ -180,12 +180,12 @@
 
         case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
-          val (doc_edits, version) =
+          val (syntax_changed, doc_edits, version) =
             Timing.timeit("Thy_Load.text_edits", timing) {
               thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(version)
-          sender ! Change(doc_blobs, doc_edits, prev, version)
+          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
@@ -252,6 +252,7 @@
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
     doc_blobs: Document.Blobs,
+    syntax_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
@@ -370,9 +371,7 @@
     def handle_change(change: Change)
     //{{{
     {
-      val previous = change.previous
-      val version = change.version
-      val doc_edits = change.doc_edits
+      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
 
       def id_command(command: Command)
       {
@@ -380,7 +379,7 @@
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+          doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)
@@ -401,6 +400,8 @@
       val assignment = global_state().the_assignment(previous).check_finished
       global_state >> (_.define_version(version, assignment))
       prover.get.update(previous.id, version.id, doc_edits)
+
+      if (syntax_changed) thy_load.syntax_changed()
     }
     //}}}
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Thy/thy_load.scala	Sat Jan 25 22:18:20 2014 +0100
@@ -103,7 +103,9 @@
     reparse_limit: Int,
     previous: Document.Version,
     doc_blobs: Document.Blobs,
-    edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
     Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+  def syntax_changed() { }
 }
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jan 25 22:18:20 2014 +0100
@@ -155,8 +155,8 @@
   private def header_edits(
     base_syntax: Outer_Syntax,
     previous: Document.Version,
-    edits: List[Document.Edit_Text])
-    : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+    edits: List[Document.Edit_Text]):
+    ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
   {
     var updated_imports = false
     var updated_keywords = false
@@ -179,11 +179,14 @@
     }
 
     val syntax =
-      if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries) {
-          case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
-        }
-      else previous.syntax
+      if (previous.is_init || updated_keywords) {
+        val syntax =
+          (base_syntax /: nodes.entries) {
+            case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+          }
+        (syntax, true)
+      }
+      else (previous.syntax, false)
 
     val reparse =
       if (updated_imports || updated_keywords)
@@ -428,13 +431,13 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text])
-    : (List[Document.Edit_Command], Document.Version) =
+    : (Boolean, List[Document.Edit_Command], Document.Version) =
   {
-    val (syntax, reparse0, nodes0, doc_edits0) =
+    val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
       header_edits(thy_load.base_syntax, previous, edits)
 
     if (edits.isEmpty)
-      (Nil, Document.Version.make(syntax, previous.nodes))
+      (false, Nil, Document.Version.make(syntax, previous.nodes))
     else {
       val reparse =
         (reparse0 /: nodes0.entries)({
@@ -472,7 +475,7 @@
           nodes += (name -> node2)
       }
 
-      (doc_edits.toList, Document.Version.make(syntax, nodes))
+      (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
     }
   }
 }
diff -r ee5a0ca00b6f -r de95c97efab3 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -6,8 +6,8 @@
 
 signature BASIC_RULE_INSTS =
 sig
-  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
-  val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
+  val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
+  val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
   val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
   val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
   val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
@@ -20,6 +20,10 @@
 signature RULE_INSTS =
 sig
   include BASIC_RULE_INSTS
+  val where_rule: Proof.context -> (indexname * string) list ->
+    (binding * string option * mixfix) list -> thm -> thm
+  val of_rule: Proof.context -> string option list * string option list ->
+    (binding * string option * mixfix) list -> thm -> thm
   val make_elim_preserve: thm -> thm
   val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
@@ -123,9 +127,10 @@
     (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
   end;
 
-fun read_instantiate_mixed ctxt mixed_insts thm =
+fun where_rule ctxt mixed_insts fixes thm =
   let
     val ctxt' = ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
       |> Variable.declare_thm thm
       |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
     val tvars = Thm.fold_terms Term.add_tvars thm [];
@@ -133,10 +138,11 @@
     val insts = read_insts ctxt' mixed_insts (tvars, vars);
   in
     Drule.instantiate_normalize insts thm
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Rule_Cases.save thm
   end;
 
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+fun of_rule ctxt (args, concl_args) fixes thm =
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
@@ -145,17 +151,18 @@
     val insts =
       zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
       zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
-  in read_instantiate_mixed ctxt insts thm end;
+  in where_rule ctxt insts fixes thm end;
 
 end;
 
 
 (* instantiation of rule or goal state *)
 
-fun read_instantiate ctxt =
-  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic);  (* FIXME !? *)
+fun read_instantiate ctxt insts xs =
+  where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
 
-fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+fun instantiate_tac ctxt insts fixes =
+  PRIMITIVE (read_instantiate ctxt insts fixes);
 
 
 
@@ -165,9 +172,10 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding "where"}
-    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
-      (fn args =>
-        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+    (Scan.lift
+      (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >>
+      (fn (insts, fixes) =>
+        Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
     "named instantiation of theorem");
 
 
@@ -186,8 +194,8 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding "of"}
-    (Scan.lift insts >> (fn args =>
-      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+    (Scan.lift (insts -- Parse.for_fixes) >> (fn (args, fixes) =>
+      Thm.rule_attribute (fn context => of_rule (Context.proof_of context) args fixes)))
     "positional instantiation of theorem");
 
 end;
diff -r ee5a0ca00b6f -r de95c97efab3 src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jan 25 22:18:20 2014 +0100
@@ -14,7 +14,7 @@
 
 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.{View, Buffer}
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
@@ -111,5 +111,11 @@
       }
     content()
   }
+
+
+  /* theory text edits */
+
+  override def syntax_changed(): Unit =
+    Swing_Thread.later { jEdit.propertiesChanged() }
 }
 
diff -r ee5a0ca00b6f -r de95c97efab3 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat Jan 25 19:07:07 2014 +0100
+++ b/src/ZF/ind_syntax.ML	Sat Jan 25 22:18:20 2014 +0100
@@ -50,7 +50,7 @@
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD =
-    read_instantiate @{context} [(("W", 0), "?Q")]
+    read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));