# HG changeset patch
# User wenzelm
# Date 1394140501 -3600
# Node ID 0c2c61a87a7d9c585690c9088e79520a083a8709
# Parent  5163ed3a38f55df10bbf4198626ca6935b3c05e0# Parent  acdde1a5faa09c4ce306ebcc23d41cb271a1be2b
merged

diff -r 5163ed3a38f5 -r 0c2c61a87a7d NEWS
--- a/NEWS	Thu Mar 06 17:55:39 2014 +0100
+++ b/NEWS	Thu Mar 06 22:15:01 2014 +0100
@@ -40,6 +40,13 @@
 completion for ML source, but within ML strings, comments,
 antiquotations.
 
+* Semantic completions may get extended by appending a suffix of
+underscores to an already recognized name, e.g. "foo_" to complete
+"foo" or "foobar" if these are known in the context.  The special
+identifier "__" serves as a wild-card in this respect: it completes to
+the full collection of names from the name space (truncated according
+to the system option "completion_limit").
+
 * Document panel: simplied interaction where every single mouse click
 (re)opens document via desktop environment or as jEdit buffer.
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 22:15:01 2014 +0100
@@ -46,7 +46,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const_proper ctxt false c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Mar 06 22:15:01 2014 +0100
@@ -881,9 +881,9 @@
   assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
   shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
   using qe_inv DJ_qe[OF qe_inv]
-  by(induct p rule: qelim.induct)
-  (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
-    simpfm simpfm_qf simp del: simpfm.simps)
+  by (induct p rule: qelim.induct)
+    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
+      simpfm simpfm_qf simp del: simpfm.simps)
 
 text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
 
@@ -908,7 +908,7 @@
 | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
 
 lemma zsplit0_I:
-  shows "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
+  "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
     (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
   (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
 proof (induct t rule: zsplit0.induct)
@@ -930,11 +930,11 @@
   moreover
   {
     assume m0: "m = 0"
-    with abj have th: "a'=?b \<and> n=i+?j" using 3
-      by (simp add: Let_def split_def)
+    with abj have th: "a' = ?b \<and> n = i + ?j"
+      using 3 by (simp add: Let_def split_def)
     from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b"
       by blast
-    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)"
+    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
       by simp
     also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
       by (simp add: distrib_right)
@@ -948,8 +948,9 @@
   case (4 t n a)
   let ?nt = "fst (zsplit0 t)"
   let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp
-  then have th: "a=Neg ?at \<and> n=-?nt"
+  have abj: "zsplit0 t = (?nt, ?at)"
+    by simp
+  then have th: "a = Neg ?at \<and> n = - ?nt"
     using 4 by (simp add: Let_def split_def)
   from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
     by blast
@@ -965,9 +966,9 @@
     by simp
   moreover have abjt: "zsplit0 t = (?nt, ?at)"
     by simp
-  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt"
+  ultimately have th: "a = Add ?as ?at \<and> n = ?ns + ?nt"
     using 5 by (simp add: Let_def split_def)
-  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
+  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
     by blast
   from 5 have "(\<exists>x y. (x, y) = zsplit0 s) \<longrightarrow>
     (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
@@ -988,9 +989,9 @@
     by simp
   moreover have abjt: "zsplit0 t = (?nt, ?at)"
     by simp
-  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt"
+  ultimately have th: "a = Sub ?as ?at \<and> n = ?ns - ?nt"
     using 6 by (simp add: Let_def split_def)
-  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
+  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
     by blast
   from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
     (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
@@ -1007,7 +1008,7 @@
   let ?at = "snd (zsplit0 t)"
   have abj: "zsplit0 t = (?nt,?at)"
     by simp
-  then have th: "a=Mul i ?at \<and> n=i*?nt"
+  then have th: "a = Mul i ?at \<and> n = i * ?nt"
     using 7 by (simp add: Let_def split_def)
   from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
     by blast
@@ -1042,34 +1043,50 @@
   "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
   "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
-  "zlfm (Lt a) = (let (c,r) = zsplit0 a in
-     if c=0 then Lt r else
-     if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
-  "zlfm (Le a) = (let (c,r) = zsplit0 a in
-     if c=0 then Le r else
-     if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
-  "zlfm (Gt a) = (let (c,r) = zsplit0 a in
-     if c=0 then Gt r else
-     if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
-  "zlfm (Ge a) = (let (c,r) = zsplit0 a in
-     if c=0 then Ge r else
-     if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
-  "zlfm (Eq a) = (let (c,r) = zsplit0 a in
-     if c=0 then Eq r else
-     if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
-  "zlfm (NEq a) = (let (c,r) = zsplit0 a in
-     if c=0 then NEq r else
-     if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
-  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
-        else (let (c,r) = zsplit0 a in
-              if c=0 then (Dvd (abs i) r) else
-      if c>0 then (Dvd (abs i) (CN 0 c r))
-      else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
-  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
-        else (let (c,r) = zsplit0 a in
-              if c=0 then (NDvd (abs i) r) else
-      if c>0 then (NDvd (abs i) (CN 0 c r))
-      else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
+  "zlfm (Lt a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then Lt r else
+      if c > 0 then (Lt (CN 0 c r))
+      else Gt (CN 0 (- c) (Neg r)))"
+  "zlfm (Le a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then Le r
+      else if c > 0 then Le (CN 0 c r)
+      else Ge (CN 0 (- c) (Neg r)))"
+  "zlfm (Gt a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then Gt r else
+      if c > 0 then Gt (CN 0 c r)
+      else Lt (CN 0 (- c) (Neg r)))"
+  "zlfm (Ge a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then Ge r
+      else if c > 0 then Ge (CN 0 c r)
+      else Le (CN 0 (- c) (Neg r)))"
+  "zlfm (Eq a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then Eq r
+      else if c > 0 then Eq (CN 0 c r)
+      else Eq (CN 0 (- c) (Neg r)))"
+  "zlfm (NEq a) =
+    (let (c, r) = zsplit0 a in
+      if c = 0 then NEq r
+      else if c > 0 then NEq (CN 0 c r)
+      else NEq (CN 0 (- c) (Neg r)))"
+  "zlfm (Dvd i a) =
+    (if i = 0 then zlfm (Eq a)
+     else
+      let (c, r) = zsplit0 a in
+        if c = 0 then Dvd (abs i) r
+        else if c > 0 then Dvd (abs i) (CN 0 c r)
+        else Dvd (abs i) (CN 0 (- c) (Neg r)))"
+  "zlfm (NDvd i a) =
+    (if i = 0 then zlfm (NEq a)
+     else
+      let (c, r) = zsplit0 a in
+        if c = 0 then NDvd (abs i) r
+        else if c > 0 then NDvd (abs i) (CN 0 c r)
+        else NDvd (abs i) (CN 0 (- c) (Neg r)))"
   "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
@@ -1091,7 +1108,7 @@
 
 lemma zlfm_I:
   assumes qfp: "qfree p"
-  shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
+  shows "(Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p) \<and> iszlfm (zlfm p)"
   (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
   using qfp
 proof (induct p rule: zlfm.induct)
@@ -1101,10 +1118,10 @@
   have spl: "zsplit0 a = (?c, ?r)"
     by simp
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
-  from 5 Ia nb  show ?case
+  let ?N = "\<lambda>t. Inum (i # bs) t"
+  from 5 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
@@ -1118,9 +1135,9 @@
   have spl: "zsplit0 a = (?c, ?r)"
     by simp
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   from 6 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
@@ -1137,7 +1154,7 @@
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   from 7 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
@@ -1152,9 +1169,9 @@
   have spl: "zsplit0 a = (?c, ?r)"
     by simp
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
+  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   from 8 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
@@ -1171,7 +1188,7 @@
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   from 9 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
@@ -1188,7 +1205,7 @@
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   from 10 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
@@ -1255,13 +1272,13 @@
   from zsplit0_I[OF spl, where x="i" and bs="bs"]
   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
     by auto
-  let ?N = "\<lambda>t. Inum (i#bs) t"
+  let ?N = "\<lambda>t. Inum (i # bs) t"
   have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
     by arith
   moreover
   {
     assume "j = 0"
-    then have z: "zlfm (NDvd j a) = (zlfm (NEq a))"
+    then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
       by (simp add: Let_def)
     then have ?case
       using assms 12 `j = 0` by (simp del: zlfm.simps)
@@ -1484,17 +1501,17 @@
 lemma minusinf_inf:
   assumes linp: "iszlfm p"
     and u: "d_\<beta> p 1"
-  shows "\<exists>(z::int). \<forall>x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
+  shows "\<exists>z::int. \<forall>x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
   (is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
   using linp u
 proof (induct p rule: minusinf.induct)
   case (1 p q)
   then show ?case
-    by auto (rule_tac x="min z za" in exI, simp)
+    by auto (rule_tac x = "min z za" in exI, simp)
 next
   case (2 p q)
   then show ?case
-    by auto (rule_tac x="min z za" in exI, simp)
+    by auto (rule_tac x = "min z za" in exI, simp)
 next
   case (3 c e)
   then have c1: "c = 1" and nb: "numbound0 e"
@@ -1513,10 +1530,10 @@
   then have c1: "c = 1" and nb: "numbound0 e"
     by simp_all
   fix a
-  from 4 have "\<forall>x < (- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
+  from 4 have "\<forall>x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
   proof clarsimp
     fix x
-    assume "x < (- Inum (a#bs) e)" and"x + Inum (x # bs) e = 0"
+    assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "False" by simp
   qed
@@ -1526,10 +1543,10 @@
   then have c1: "c = 1" and nb: "numbound0 e"
     by simp_all
   fix a
-  from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
+  from 5 have "\<forall>x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
   proof clarsimp
     fix x
-    assume "x < (- Inum (a#bs) e)"
+    assume "x < (- Inum (a # bs) e)"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "x + Inum (x # bs) e < 0"
       by simp
@@ -1540,12 +1557,12 @@
   then have c1: "c = 1" and nb: "numbound0 e"
     by simp_all
   fix a
-  from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
+  from 6 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<le> 0"
   proof clarsimp
     fix x
-    assume "x < (- Inum (a#bs) e)"
+    assume "x < (- Inum (a # bs) e)"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
-    show "x + Inum (x#bs) e \<le> 0" by simp
+    show "x + Inum (x # bs) e \<le> 0" by simp
   qed
   then show ?case by auto
 next
@@ -1553,10 +1570,10 @@
   then have c1: "c = 1" and nb: "numbound0 e"
     by simp_all
   fix a
-  from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
+  from 7 have "\<forall>x<(- Inum (a # bs) e). \<not> (c * x + Inum (x # bs) e > 0)"
   proof clarsimp
     fix x
-    assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
+    assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show False by simp
   qed
@@ -1596,23 +1613,23 @@
       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
     then have "\<exists>l::int. ?rt = i * l"
       by (simp add: dvd_def)
-    then have "\<exists>l::int. c*x+ ?I x e = i * l + c * (k * i * di)"
+    then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
       by (simp add: algebra_simps di_def)
-    then have "\<exists>l::int. c*x+ ?I x e = i*(l + c * k * di)"
+    then have "\<exists>l::int. c * x + ?I x e = i* (l + c * k * di)"
       by (simp add: algebra_simps)
     then have "\<exists>l::int. c * x + ?I x e = i * l"
       by blast
     then show "i dvd c * x + Inum (x # bs) e"
       by (simp add: dvd_def)
   next
-    assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
+    assume "i dvd c * x + Inum (x # bs) e"  (is "?ri dvd ?rc * ?rx + ?e")
     then have "\<exists>l::int. c * x + ?e = i * l"
       by (simp add: dvd_def)
     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
       by simp
     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
       by (simp add: di_def)
-    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
       by (simp add: algebra_simps)
     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
       by blast
@@ -1660,7 +1677,7 @@
 
 lemma mirror_\<alpha>_\<beta>:
   assumes lp: "iszlfm p"
-  shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
+  shows "Inum (i # bs) ` set (\<alpha> p) = Inum (i # bs) ` set (\<beta> (mirror p))"
   using lp by (induct p rule: mirror.induct) auto
 
 lemma mirror:
@@ -1669,27 +1686,30 @@
   using lp
 proof (induct p rule: iszlfm.induct)
   case (9 j c e)
-  then have nb: "numbound0 e" by simp
-  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
+  then have nb: "numbound0 e"
+    by simp
+  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
     (is "_ = (j dvd c*x - ?e)") by simp
-  also have "\<dots> = (j dvd (- (c*x - ?e)))"
+  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
     by (simp only: dvd_minus_iff)
-  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
+  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
     by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
       (simp add: algebra_simps)
-  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
+  also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
   finally show ?case .
 next
-  case (10 j c e) then have nb: "numbound0 e" by simp
-  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
-    (is "_ = (j dvd c*x - ?e)") by simp
-  also have "\<dots> = (j dvd (- (c*x - ?e)))"
+  case (10 j c e)
+  then have nb: "numbound0 e"
+    by simp
+  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
+    (is "_ = (j dvd c * x - ?e)") by simp
+  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
     by (simp only: dvd_minus_iff)
-  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
+  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
     by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
       (simp add: algebra_simps)
-  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
+  also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
   finally show ?case by simp
 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
@@ -1702,7 +1722,7 @@
 
 lemma \<beta>_numbound0:
   assumes lp: "iszlfm p"
-  shows "\<forall>b\<in> set (\<beta> p). numbound0 b"
+  shows "\<forall>b \<in> set (\<beta> p). numbound0 b"
   using lp by (induct p rule: \<beta>.induct) auto
 
 lemma d_\<beta>_mono:
@@ -1724,29 +1744,37 @@
   using linp
 proof (induct p rule: iszlfm.induct)
   case (1 p q)
-  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
+    by simp
+  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
+    by simp
   from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
-    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
-    dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
+      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+      dl1 dl2
+  show ?case
+    by (auto simp add: lcm_pos_int)
 next
   case (2 p q)
-  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
+    by simp
+  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
+    by simp
   from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
-    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
-    dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
+      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+      dl1 dl2
+  show ?case
+    by (auto simp add: lcm_pos_int)
 qed (auto simp add: lcm_pos_int)
 
 lemma a_\<beta>:
   assumes linp: "iszlfm p"
     and d: "d_\<beta> p l"
     and lp: "l > 0"
-  shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)"
+  shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> Ifm bbs (l * x # bs) (a_\<beta> p l) = Ifm bbs (x # bs) p"
   using linp d
 proof (induct p rule: iszlfm.induct)
   case (5 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l"
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
     by simp_all
   from lp cp have clel: "c \<le> l"
     by (simp add: zdvd_imp_le [OF d' lp])
@@ -1760,15 +1788,17 @@
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
-  then have "(l*x + (l div c) * Inum (x # bs) e < 0) =
+  then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
     by simp
-  also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
-    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
+    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
+    by simp
   finally show ?case
-    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
+    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
+    by simp
 next
   case (6 c e)
   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
@@ -1777,20 +1807,20 @@
     by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0"
     by simp
-  have "c div c\<le> l div c"
+  have "c div c \<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
-  then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
+  then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
+      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
     by simp
-  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<le> 0"
     using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
   finally show ?case
     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
@@ -1804,18 +1834,18 @@
     by simp
   have "c div c \<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
-  then have ldcp:"0 < l div c"
+  then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  then have cl:"c * (l div c) = l"
+  then have cl: "c * (l div c) = l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
-  then have "(l * x + (l div c) * Inum (x # bs) e > 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
+  then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
+      (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
     by simp
-  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e > 0"
     using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
     by simp
   finally show ?case
@@ -1833,17 +1863,17 @@
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
-      ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
+  then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
+      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
     by simp
-  also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<ge> 0"
     using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
     by simp
   finally show ?case
@@ -1861,16 +1891,16 @@
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
+  then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
+      (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
     by simp
-  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e = 0"
     using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
     by simp
   finally show ?case
@@ -1888,11 +1918,11 @@
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
-  then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) \<longleftrightarrow>
+  then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
@@ -1914,14 +1944,14 @@
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c"
+  have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
-      (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
+      (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     by simp
-  also have "\<dots> \<longleftrightarrow> (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
     by (simp add: algebra_simps)
   also
   fix k
@@ -1958,10 +1988,10 @@
     by (simp add: algebra_simps)
   also
   fix k
-  have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
+  have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
     by simp
-  also have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
     by simp
   finally show ?case
     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
@@ -1988,15 +2018,15 @@
     and u: "d_\<beta> p 1"
     and d: "d_\<delta> p d"
     and dp: "d > 0"
-    and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
-    and p: "Ifm bbs (x#bs) p" (is "?P x")
+    and nob: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
+    and p: "Ifm bbs (x # bs) p" (is "?P x")
   shows "?P (x - d)"
   using lp u d dp nob p
 proof (induct p rule: iszlfm.induct)
   case (5 c e)
   then have c1: "c = 1" and  bn: "numbound0 e"
     by simp_all
-  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
+  with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5
   show ?case by simp
 next
   case (6 c e)
@@ -2006,29 +2036,30 @@
   show ?case by simp
 next
   case (7 c e)
-  then have p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
+  then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
     by simp_all
   let ?e = "Inum (x # bs) e"
   {
-    assume "(x-d) +?e > 0"
+    assume "(x - d) + ?e > 0"
     then have ?case
       using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
   }
   moreover
   {
-    assume H: "\<not> (x-d) + ?e > 0"
-    let ?v="Neg e"
-    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
+    assume H: "\<not> (x - d) + ?e > 0"
+    let ?v = "Neg e"
+    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
+      by simp
     from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
-    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e + j)"
+    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
       by auto
     from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
       by (simp add: c1)
     then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
       by simp
-    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e"
+    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e"
       by simp
-    then have "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
+    then have "\<exists>j::int \<in> {1 .. d}. x = (- ?e + j)"
       by (simp add: algebra_simps)
     with nob have ?case
       by auto
@@ -2059,9 +2090,9 @@
       by (simp add: c1)
     then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
       by simp
-    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1"
+    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e + 1"
       by simp
-    then have "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j"
+    then have "\<exists>j::int \<in> {1 .. d}. x= - ?e - 1 + j"
       by (simp add: algebra_simps)
     with nob have ?case
       by simp
@@ -2072,35 +2103,38 @@
   case (3 c e)
   then
   have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
-    and c1: "c=1"
+    and c1: "c = 1"
     and bn: "numbound0 e"
     by simp_all
   let ?e = "Inum (x # bs) e"
   let ?v="(Sub (C -1) e)"
   have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
     by simp
-  from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case
+  from p have "x= - ?e"
+    by (simp add: c1) with 3(5)
+  show ?case
     using dp
     by simp (erule ballE[where x="1"],
       simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
 next
   case (4 c e)
   then
-  have p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x")
+  have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x")
     and c1: "c = 1"
     and bn: "numbound0 e"
     by simp_all
   let ?e = "Inum (x # bs) e"
   let ?v="Neg e"
-  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
+  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))"
+    by simp
   {
     assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
     then have ?case by (simp add: c1)
   }
   moreover
   {
-    assume H: "x - d + Inum (((x -d)) # bs) e = 0"
-    then have "x = - Inum (((x -d)) # bs) e + d"
+    assume H: "x - d + Inum ((x - d) # bs) e = 0"
+    then have "x = - Inum ((x - d) # bs) e + d"
       by simp
     then have "x = - Inum (a # bs) e + d"
       by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
@@ -2119,9 +2153,9 @@
   let ?e = "Inum (x # bs) e"
   from 9 have id: "j dvd d"
     by simp
-  from c1 have "?p x = (j dvd (x + ?e))"
+  from c1 have "?p x \<longleftrightarrow> j dvd (x + ?e)"
     by simp
-  also have "\<dots> = (j dvd x - d + ?e)"
+  also have "\<dots> \<longleftrightarrow> j dvd x - d + ?e"
     using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
     by simp
   finally show ?case
@@ -2130,16 +2164,16 @@
 next
   case (10 j c e)
   then
-  have p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x")
+  have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x")
     and c1: "c = 1"
     and bn: "numbound0 e"
     by simp_all
   let ?e = "Inum (x # bs) e"
   from 10 have id: "j dvd d"
     by simp
-  from c1 have "?p x = (\<not> j dvd (x + ?e))"
+  from c1 have "?p x \<longleftrightarrow> \<not> j dvd (x + ?e)"
     by simp
-  also have "\<dots> = (\<not> j dvd x - d + ?e)"
+  also have "\<dots> \<longleftrightarrow> \<not> j dvd x - d + ?e"
     using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
     by simp
   finally show ?case
@@ -2152,13 +2186,13 @@
   and u: "d_\<beta> p 1"
   and d: "d_\<delta> p d"
   and dp: "d > 0"
-  shows "\<forall>x. \<not> (\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
-    Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
+  shows "\<forall>x. \<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
+    Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
 proof clarify
   fix x
   assume nb: "?b"
     and px: "?P x"
-  then have nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
+  then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
     by auto
   from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
 qed
@@ -2191,16 +2225,18 @@
     and u: "d_\<beta> p 1"
     and d: "d_\<delta> p d"
     and dp: "d > 0"
-  shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
+  shows "(\<exists>(x::int). Ifm bbs (x # bs) p) \<longleftrightarrow>
+    (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
+      (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
   (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
 proof -
   from minusinf_inf[OF lp u]
-  have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x"
+  have th: "\<exists>z::int. \<forall>x<z. ?P (x) = ?M x"
     by blast
-  let ?B' = "{?I b | b. b\<in> ?B}"
-  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
+  let ?B' = "{?I b | b. b \<in> ?B}"
+  have BB': "(\<exists>j\<in>?D. \<exists>b \<in> ?B. ?P (?I b + j)) \<longleftrightarrow> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
     by auto
-  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
+  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)"
     using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
   from minusinf_repeats[OF d lp]
   have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
@@ -2214,31 +2250,50 @@
   assumes lp: "iszlfm p"
   shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
   (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
-proof(auto)
-  fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF lp] by blast
-  then show "\<exists>x. ?I x p" by blast
+proof auto
+  fix x
+  assume "?I x ?mp"
+  then have "?I (- x) p"
+    using mirror[OF lp] by blast
+  then show "\<exists>x. ?I x p"
+    by blast
 next
-  fix x assume "?I x p" then have "?I (- x) ?mp"
+  fix x
+  assume "?I x p"
+  then have "?I (- x) ?mp"
     using mirror[OF lp, where x="- x", symmetric] by auto
-  then show "\<exists>x. ?I x ?mp" by blast
+  then show "\<exists>x. ?I x ?mp"
+    by blast
 qed
 
-
 lemma cp_thm':
   assumes lp: "iszlfm p"
-  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
-  shows "(\<exists>x. Ifm bbs (x#bs) p) = ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))"
+    and up: "d_\<beta> p 1"
+    and dd: "d_\<delta> p d"
+    and dp: "d > 0"
+  shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
+    ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
+      (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
   using cp_thm[OF lp up dd dp,where i="i"] by auto
 
 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
 where
-  "unit p = (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
-             B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
-             in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
+  "unit p =
+     (let
+        p' = zlfm p;
+        l = \<zeta> p';
+        q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l);
+        d = \<delta> q;
+        B = remdups (map simpnum (\<beta> q));
+        a = remdups (map simpnum (\<alpha> q))
+      in if length B \<le> length a then (q, B, d) else (mirror q, a, d))"
 
 lemma unit:
   assumes qf: "qfree p"
-  shows "\<And>q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
+  shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
+    ((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
+    (Inum (i # bs)) ` set B = (Inum (i # bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d > 0 \<and>
+    iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
 proof -
   fix q B d
   assume qBd: "unit p = (q,B,d)"
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 22:15:01 2014 +0100
@@ -100,7 +100,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const_proper ctxt false c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -185,7 +185,7 @@
      (Scan.succeed false);
 
 fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.type_name true >>
+  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
     (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
 fun setup_fresh_fun_simp x =
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -63,7 +63,7 @@
   let
     val tune =
       if internal then Name.internal
-      else fn x => the_default x (try Name.dest_internal x);
+      else perhaps (try Name.dest_internal);
     val n = length xs;
     fun rename prem =
       let
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -33,7 +33,8 @@
       error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
 
     val fpT_names =
-      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
+      map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
+        raw_fpT_names;
 
     fun lfp_sugar_of s =
       (case fp_sugar_of lthy s of
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -234,7 +234,7 @@
 (** document antiquotation **)
 
 val antiq_setup =
-  Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
+  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
     (fn {source = src, context = ctxt, ...} => fn dtco =>
       let
         val thy = Proof_Context.theory_of ctxt;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -534,10 +534,11 @@
         (drop (length dt_names) inducts);
 
     val ctxt = Proof_Context.init_global thy9;
-    val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
+    val case_combs =
+      map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
     val constrss = map (fn (dtname, {descr, index, ...}) =>
-      map (Proof_Context.read_const ctxt false dummyT o fst)
-        (#3 (the (AList.lookup op = descr index)))) dt_infos
+      map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
+        (#3 (the (AList.lookup op = descr index)))) dt_infos;
   in
     thy9
     |> Global_Theory.note_thmss ""
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -61,8 +61,10 @@
 
 val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
   
-val quickcheck_generator_cmd = gen_quickcheck_generator
-  (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+val quickcheck_generator_cmd =
+  gen_quickcheck_generator
+    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
+    Syntax.read_term
   
 val _ =
   Outer_Syntax.command @{command_spec "quickcheck_generator"}
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -71,8 +71,9 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding mapQ3}
-    ((Args.type_name true --| Scan.lift @{keyword "="}) --
-      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+    ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
+      (Scan.lift @{keyword "("} |--
+        Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
         Attrib.thm --| Scan.lift @{keyword ")"}) >>
       (fn (tyname, (relname, qthm)) =>
         let val minfo = {relmap = relname, quot_thm = qthm}
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -430,7 +430,7 @@
   | NONE => [ax])
 
 fun external_frees t =
-  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
+  [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
 
 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   if Config.get ctxt instantiate_inducts then
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -144,7 +144,7 @@
         val do_preplay = preplay_timeout <> Time.zeroTime
         val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
 
-        val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+        val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
         fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
 
         fun get_role keep_role ((num, _), role, t, rule, _) =
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -129,9 +129,9 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule Induct.typeN (Args.type_name false) get_type ||
-  named_rule Induct.predN (Args.const false) get_pred ||
-  named_rule Induct.setN (Args.const false) get_pred ||
+  named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
+  named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
+  named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -515,7 +515,8 @@
 val setup =
   Attrib.setup @{binding ind_realizer}
     ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
-      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
+      Scan.option (Scan.lift (Args.colon) |--
+        Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
     "add realizers for inductive set";
 
 end;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -56,7 +56,7 @@
   val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table
   val check_reports: Context.generic -> 'a table ->
-    xstring * Position.T -> (string * Position.report list) * 'a
+    xstring * Position.T list -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -205,7 +205,7 @@
 (* completion *)
 
 fun completion context space (xname, pos) =
-  if Context_Position.is_reported_generic context pos then
+  if Position.is_reported pos then
     let
       val x = Name.clean xname;
       val Name_Space {kind = k, internals, ...} = space;
@@ -322,6 +322,8 @@
 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   | transform_binding _ = I;
 
+val bad_specs = ["", "??", "__"];
+
 fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
     val binding = transform_binding naming raw_binding;
@@ -332,7 +334,7 @@
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
-      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
+      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso err_bad binding;
   in (concealed, if null spec2 then [] else spec) end;
 
@@ -446,24 +448,27 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun check_reports context (space, tab) (xname, pos) =
+fun check_reports context (space, tab) (xname, ps) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
       SOME x =>
         let
           val reports =
-            if Context_Position.is_reported_generic context pos
-            then [(pos, markup space name)] else [];
+            filter (Context_Position.is_reported_generic context) ps
+            |> map (fn pos => (pos, markup space name));
         in ((name, reports), x) end
     | NONE =>
-        error (undefined (kind_of space) name ^ Position.here pos ^
-          Markup.markup Markup.report
-            (Completion.reported_text (completion context space (xname, pos)))))
+        let
+          val completions = map (fn pos => completion context space (xname, pos)) ps;
+        in
+          error (undefined (kind_of space) name ^ Position.here_list ps ^
+            Markup.markup_report (implode (map Completion.reported_text completions)))
+        end)
   end;
 
-fun check context table arg =
+fun check context table (xname, pos) =
   let
-    val ((name, reports), x) = check_reports context table arg;
+    val ((name, reports), x) = check_reports context table (xname, [pos]);
     val _ = Position.reports reports;
   in (name, x) end;
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/General/position.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -43,6 +43,7 @@
   val reports: report list -> unit
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
+  val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
@@ -182,6 +183,9 @@
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
+fun append_reports (r: report_text list Unsynchronized.ref) reports =
+  Unsynchronized.change r (append (map (rpair "") reports));
+
 
 (* here: inlined formal markup *)
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -56,9 +56,8 @@
   val term_pattern: term context_parser
   val term_abbrev: term context_parser
   val prop: term context_parser
-  val type_name: bool -> string context_parser
-  val const: bool -> string context_parser
-  val const_proper: bool -> string context_parser
+  val type_name: {proper: bool, strict: bool} -> string context_parser
+  val const: {proper: bool, strict: bool} -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: Token.T list parser
   val parse1: (string -> bool) -> Token.T list parser
@@ -208,18 +207,14 @@
 
 (* type and constant names *)
 
-fun type_name strict =
-  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
+fun type_name flags =
+  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
-fun const strict =
-  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
+fun const flags =
+  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
-fun const_proper strict =
-  Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
-  >> (fn Const (c, _) => c | _ => "");
-
 
 (* improper method arguments *)
 
@@ -304,7 +299,7 @@
     | (_, (_, args2)) =>
         error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
           (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
-          Markup.markup Markup.report (reported_text ())))
+          Markup.markup_report (reported_text ())))
   end;
 
 fun context_syntax kind scan src =
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -575,13 +575,17 @@
   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
   #> reset_facts;
 
+fun read_arg ctxt (c, mx) =
+  (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
+    Free (x, _) =>
+      let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
+      in (Free (x, T), mx) end
+  | t => (t, mx));
+
 in
 
 val write = gen_write (K I);
-
-val write_cmd =
-  gen_write (fn ctxt => fn (c, mx) =>
-    (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
+val write_cmd = gen_write read_arg;
 
 end;
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -68,21 +68,19 @@
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
-  val check_type_name: Proof.context -> bool ->
-    xstring * Position.T -> typ * Position.report list
-  val check_type_name_proper: Proof.context -> bool ->
+  val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     xstring * Position.T -> typ * Position.report list
-  val read_type_name: Proof.context -> bool -> string -> typ
-  val read_type_name_proper: Proof.context -> bool -> string -> typ
-  val read_const_proper: Proof.context -> bool -> string -> term
-  val read_const: Proof.context -> bool -> typ -> string -> term
+  val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
+  val consts_completion_message: Proof.context -> xstring * Position.T list -> string
+  val check_const: Proof.context -> {proper: bool, strict: bool} ->
+    xstring * Position.T list -> term * Position.report list
+  val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
   val prepare_sortsT: Proof.context -> typ list -> string * typ list
   val prepare_sorts: Proof.context -> term list -> string * term list
   val check_tfree: Proof.context -> string * sort -> string * sort
-  val intern_skolem: Proof.context -> string -> string option
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
@@ -387,9 +385,8 @@
     val name = Type.cert_class tsig (Type.intern_class tsig xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
-          Markup.markup Markup.report
-            (Completion.reported_text
-              (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
+          Markup.markup_report (Completion.reported_text
+            (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
@@ -422,19 +419,6 @@
 
 
 
-(** prepare variables **)
-
-(* check Skolem constants *)
-
-fun no_skolem internal x =
-  if can Name.dest_skolem x then
-    error ("Illegal reference to internal Skolem constant: " ^ quote x)
-  else if not internal andalso can Name.dest_internal x then
-    error ("Illegal reference to internal variable: " ^ quote x)
-  else x;
-
-
-
 (** prepare terms and propositions **)
 
 (* inferred types of parameters *)
@@ -455,13 +439,15 @@
 
 (* type names *)
 
-fun check_type_name ctxt strict (c, pos) =
+fun check_type_name ctxt {proper, strict} (c, pos) =
   if Lexicon.is_tid c then
-    let
-      val reports =
-        if Context_Position.is_reported ctxt pos
-        then [(pos, Markup.tfree)] else [];
-    in (TFree (c, default_sort ctxt (c, ~1)), reports) end
+    if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
+    else
+      let
+        val reports =
+          if Context_Position.is_reported ctxt pos
+          then [(pos, Markup.tfree)] else [];
+      in (TFree (c, default_sort ctxt (c, ~1)), reports) end
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
@@ -473,59 +459,61 @@
         | Type.Nonterminal => if strict then err () else 0);
     in (Type (d, replicate args dummyT), reports) end;
 
-fun check_type_name_proper ctxt strict arg =
-  (case check_type_name ctxt strict arg of
-    res as (Type _, _) => res
-  | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
-
-fun read_type_name ctxt strict =
-  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1;
-
-fun read_type_name_proper ctxt strict =
-  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1;
+fun read_type_name ctxt flags text =
+  let
+    val (T, reports) =
+      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+    val _ = Position.reports reports;
+  in T end;
 
 
 (* constant names *)
 
-local
-
-fun prep_const_proper ctxt strict (c, pos) =
-  let
-    fun err msg = error (msg ^ Position.here pos);
-    val consts = consts_of ctxt;
-    val t as Const (d, _) =
-      (case Variable.lookup_const ctxt c of
-        SOME d =>
-          let
-            val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
-            val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
-          in Const (d, T) end
-      | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
-    val _ =
-      if strict
-      then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
-      else ();
-  in t end;
+fun consts_completion_message ctxt (c, ps) =
+  ps |> map (fn pos =>
+    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+    |> Completion.reported_text)
+  |> implode
+  |> Markup.markup_report;
 
-in
-
-fun read_const_proper ctxt strict =
-  prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
-
-fun read_const ctxt strict ty text =
+fun check_const ctxt {proper, strict} (c, ps) =
   let
-    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-    val _ = no_skolem false c;
-  in
-    (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
-      (SOME x, false) =>
-        (Context_Position.report ctxt pos
-            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
-          Free (x, infer_type ctxt (x, ty)))
-    | _ => prep_const_proper ctxt strict (c, pos))
-  end;
+    val _ =
+      Name.reject_internal (c, ps) handle ERROR msg =>
+        error (msg ^ consts_completion_message ctxt (c, ps));
+    fun err msg = error (msg ^ Position.here_list ps);
+    val consts = consts_of ctxt;
+    val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
+    val (t, reports) =
+      (case (fixed, Variable.lookup_const ctxt c) of
+        (SOME x, NONE) =>
+          let
+            val reports = ps
+              |> filter (Context_Position.is_reported ctxt)
+              |> map (fn pos =>
+                (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
+          in (Free (x, infer_type ctxt (x, dummyT)), reports) end
+      | (_, SOME d) =>
+          let
+            val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
+            val reports = ps
+              |> filter (Context_Position.is_reported ctxt)
+              |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
+          in (Const (d, T), reports) end
+      | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
+    val _ =
+      (case (strict, t) of
+        (true, Const (d, _)) =>
+          (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
+      | _ => ());
+  in (t, reports) end;
 
-end;
+fun read_const ctxt flags text =
+  let
+    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val (t, reports) = check_const ctxt flags (xname, [pos]);
+    val _ = Position.reports reports;
+  in t end;
 
 
 (* type arities *)
@@ -539,29 +527,14 @@
 in
 
 val read_arity =
-  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+  prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
+    Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
 end;
 
 
-(* skolem variables *)
-
-fun intern_skolem ctxt x =
-  let
-    val _ = no_skolem false x;
-    val sko = Variable.lookup_fixed ctxt x;
-    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
-    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
-  in
-    if Variable.is_const ctxt x then NONE
-    else if is_some sko then sko
-    else if not is_const orelse is_declared then SOME x
-    else NONE
-  end;
-
-
 (* read_term *)
 
 fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
@@ -1033,8 +1006,10 @@
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
       val x = Variable.check_name b;
-      val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
-        error ("Illegal variable name: " ^ Binding.print b);
+      val check_name = if internal then Name.reject_skolem else Name.reject_internal;
+      val _ =
+        if can check_name (x, []) andalso Symbol_Pos.is_identifier x then ()
+        else error ("Bad name: " ^ Binding.print b);
 
       fun cond_tvars T =
         if internal then T
@@ -1375,7 +1350,7 @@
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
-        filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
+        filter_out ((Name.is_internal orf member (op =) structs) o #1)
           (Variable.dest_fixes ctxt);
       val prt_fixes =
         if null fixes then []
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -276,10 +276,12 @@
 in
 
 val type_notation = gen_type_notation (K I);
-val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
+val type_notation_cmd =
+  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
 
 val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
+val notation_cmd =
+  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
 
 end;
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -127,7 +127,7 @@
 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
+      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
       val res =
         (case try check (c, decl) of
@@ -151,7 +151,7 @@
 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
+      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
       val res = check (Proof_Context.consts_of ctxt, c)
         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     in ML_Syntax.print_string res end);
@@ -175,7 +175,8 @@
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
       >> (fn ((ctxt, raw_c), Ts) =>
         let
-          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
+          val Const (c, _) =
+            Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
           val consts = Proof_Context.consts_of ctxt;
           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
           val _ = length Ts <> n andalso
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -189,6 +189,7 @@
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markup_only: T -> string
+  val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
@@ -602,4 +603,7 @@
 
 fun markup_only m = markup m "";
 
+fun markup_report "" = ""
+  | markup_report txt = markup report txt;
+
 end;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -261,8 +261,8 @@
 fun tokenize lex xids syms =
   let
     val scan_xid =
-      if xids then $$$ "_" @@@ scan_id || scan_id
-      else scan_id;
+      (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
+      $$$ "_" @@@ $$$ "_";
 
     val scan_num = scan_hex || scan_bin || scan_int;
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -51,7 +51,7 @@
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
-  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+  [if Name.is_skolem x then Markup.skolem else Markup.free] @
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);
@@ -140,6 +140,7 @@
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report pos = Position.store_reports reports [pos];
+    val append_reports = Position.append_reports reports;
 
     fun trans a args =
       (case trf a of
@@ -164,14 +165,15 @@
           let
             val pos = Lexicon.pos_of_token tok;
             val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
-            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+            val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
             val pos = Lexicon.pos_of_token tok;
             val (Type (c, _), rs) =
-              Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
-            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+              Proof_Context.check_type_name ctxt {proper = true, strict = false}
+                (Lexicon.str_of_token tok, pos);
+            val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
@@ -220,16 +222,36 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
+fun decode_const ctxt (c, ps) =
+  let
+    val (Const (c', _), reports) =
+      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
+  in (c', reports) end;
+
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
-        fun get_const a =
-          ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
-            handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
-        val get_free = Proof_Context.intern_skolem ctxt;
-
         val reports = Unsynchronized.ref reports0;
         fun report ps = Position.store_reports reports ps;
+        val append_reports = Position.append_reports reports;
+
+        fun get_free x =
+          let
+            val fixed = Variable.lookup_fixed ctxt x;
+            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
+            val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
+          in
+            if Variable.is_const ctxt x then NONE
+            else if is_some fixed then fixed
+            else if not is_const orelse is_declared then SOME x
+            else NONE
+          end;
+
+        fun the_const (a, ps) =
+          let
+            val (c, rs) = decode_const ctxt (a, ps);
+            val _ = append_reports rs;
+          in c end;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
@@ -252,18 +274,15 @@
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
-                        SOME c => c
-                      | NONE => snd (get_const a));
-                    val _ = report ps (markup_const ctxt) c;
+                        SOME c => (report ps (markup_const ctxt) c; c)
+                      | NONE => the_const (a, ps));
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
-              (case (get_free a, get_const a) of
-                (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
-              | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
-              | (_, (false, c)) =>
-                  if Long_Name.is_qualified c
-                  then (report ps (markup_const ctxt) c; Const (c, T))
-                  else (report ps (markup_free ctxt) c; Free (c, T)))
+              ((Name.reject_internal (a, ps) handle ERROR msg =>
+                  error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
+                (case get_free a of
+                  SOME x => (report ps (markup_free ctxt) x; Free (x, T))
+                | NONE => Const (the_const (a, ps), T)))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
@@ -304,8 +323,7 @@
 
     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
-        error (msg ^
-          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+        error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
     val len = length pts;
 
     val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -337,7 +355,7 @@
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
-    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
   Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
@@ -664,7 +682,7 @@
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
   in
-    if can Name.dest_skolem x
+    if Name.is_skolem x
     then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     else ([m, Markup.free], x)
   end;
@@ -793,16 +811,15 @@
 
 (* authentic syntax *)
 
-fun const_ast_tr intern ctxt [Ast.Variable c] =
+fun const_ast_tr intern ctxt asts =
+  (case asts of
+    [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
-        val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
+        val pos = the_default Position.none (Term_Position.decode p);
+        val (c', _) = decode_const ctxt (c, [pos]);
         val d = if intern then Lexicon.mark_const c' else c;
-      in Ast.Constant d end
-  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
-      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
-        handle ERROR msg =>
-          error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
-  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
+      in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
+  | _ => raise Ast.AST ("const_ast_tr", asts));
 
 
 (* setup translations *)
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -124,7 +124,7 @@
   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
 
 fun absfree_proper (x, T) t =
-  if can Name.dest_internal x
+  if Name.is_internal x
   then error ("Illegal internal variable in abstraction: " ^ quote x)
   else absfree (x, T) t;
 
@@ -316,7 +316,7 @@
     val body = body_of tm;
     val rev_new_vars = Term.rename_wrt_term body vars;
     fun subst (x, T) b =
-      if can Name.dest_internal x andalso not (Term.is_dependent b)
+      if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
     val (rev_vars', body') = fold_map subst rev_new_vars body;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -515,7 +515,7 @@
   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
 
 fun pretty_type ctxt s =
-  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
+  let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
@@ -573,7 +573,7 @@
   basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
   basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
   basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
-  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+  basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
   basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
   basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/consts.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -25,7 +25,7 @@
   val extern: Proof.context -> T -> string -> xstring
   val intern_syntax: T -> xstring -> string
   val extern_syntax: Proof.context -> T -> string -> xstring
-  val check_const: Context.generic -> T -> xstring * Position.T -> term
+  val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
   val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
@@ -143,12 +143,12 @@
 
 (* check_const *)
 
-fun check_const context consts (xname, pos) =
+fun check_const context consts (xname, ps) =
   let
     val Consts {decls, ...} = consts;
-    val (c, _) = Name_Space.check context decls (xname, pos);
-    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
-  in Const (c, T) end;
+    val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
+    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
+  in (Const (c, T), reports) end;
 
 
 (* certify *)
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/name.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -13,8 +13,12 @@
   val is_bound: string -> bool
   val internal: string -> string
   val dest_internal: string -> string
+  val is_internal: string -> bool
+  val reject_internal: string * Position.T list -> unit
   val skolem: string -> string
   val dest_skolem: string -> string
+  val is_skolem: string -> bool
+  val reject_skolem: string * Position.T list -> unit
   val clean_index: string * int -> string * int
   val clean: string -> string
   type context
@@ -59,13 +63,19 @@
 val is_bound = String.isPrefix ":";
 
 
-(* internal names *)
+(* internal names -- NB: internal subsumes skolem *)
 
 val internal = suffix "_";
 val dest_internal = unsuffix "_";
+val is_internal = String.isSuffix "_";
+fun reject_internal (x, ps) =
+  if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
+val is_skolem = String.isSuffix "__";
+fun reject_skolem (x, ps) =
+  if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 fun clean_index (x, i) =
   (case try dest_internal x of
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/type.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -259,7 +259,8 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
+fun check_decl context (TSig {types, ...}) (c, pos) =
+  Name_Space.check_reports context types (c, [pos]);
 
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Pure/variable.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -399,7 +399,7 @@
 fun add_fixes_binding bs ctxt =
   let
     val _ =
-      (case filter (can Name.dest_skolem o Binding.name_of) bs of
+      (case filter (Name.is_skolem o Binding.name_of) bs of
         [] => ()
       | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
     val _ =
@@ -417,7 +417,7 @@
 fun variant_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;
-    val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
+    val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
     val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
   in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
 
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -97,8 +97,8 @@
       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
-fun read_tyco ctxt = #1 o dest_Type
-  o Proof_Context.read_type_name_proper ctxt true;
+fun read_tyco ctxt =
+  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
 
 fun cert_class ctxt class =
   let
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -220,7 +220,8 @@
 
 fun adhoc_overloading_cmd add raw_args lthy =
   let
-    fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
+    fun const_name ctxt =
+      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};  (* FIXME {proper = true, strict = true} (!?) *)
     fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/induct.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -361,9 +361,9 @@
   Scan.lift (Args.$$$ k) >> K "";
 
 fun attrib add_type add_pred del =
-  spec typeN (Args.type_name false) >> add_type ||
-  spec predN (Args.const false) >> add_pred ||
-  spec setN (Args.const false) >> add_pred ||
+  spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
+  spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
+  spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
   Scan.lift Args.del >> K del;
 
 in
@@ -883,9 +883,9 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule typeN (Args.type_name false) get_type ||
-  named_rule predN (Args.const false) get_pred ||
-  named_rule setN (Args.const false) get_pred ||
+  named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
+  named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
+  named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
diff -r 5163ed3a38f5 -r 0c2c61a87a7d src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/subtyping.ML	Thu Mar 06 22:15:01 2014 +0100
@@ -1105,7 +1105,7 @@
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
     "declaration of new map functions" #>
   Attrib.setup @{binding coercion_args}
-    (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
+    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
       (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
     "declaration of new constants with coercion-invariant arguments";