# HG changeset patch
# User wenzelm
# Date 1393796600 -3600
# Node ID 3a2ad5ccc1c8e075b0b73f4c4cbeaf629351ec25
# Parent  8093590e49e45d98fdce19b7cd122cf6656dd8db# Parent  1bfe72d146305ebb5dec607e415f6ea5a74b3441
merged

diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Integration.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -48,7 +48,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type Toplevel.state} \\
-  @{index_ML Toplevel.UNDEF: "exn"} \\
+  @{index_ML_exception Toplevel.UNDEF} \\
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -696,7 +696,7 @@
   abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
   same inference kernel that is mainly responsible for @{ML_type thm}.
   Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
-  are located in the @{ML_struct Thm} module, even though theorems are
+  are located in the @{ML_structure Thm} module, even though theorems are
   not yet involved at that stage.
 
   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
@@ -717,7 +717,7 @@
 
   \item Type @{ML_type thm} represents proven propositions.  This is
   an abstract datatype that guarantees that its values have been
-  constructed by basic principles of the @{ML_struct Thm} module.
+  constructed by basic principles of the @{ML_structure Thm} module.
   Every @{ML_type thm} value refers its background theory,
   cf.\ \secref{sec:context-theory}.
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -1159,8 +1159,8 @@
   \begin{mldecls}
   @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
   @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
-  @{index_ML ERROR: "string -> exn"} \\
-  @{index_ML Fail: "string -> exn"} \\
+  @{index_ML_exception ERROR: string} \\
+  @{index_ML_exception Fail: string} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
   @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
@@ -1439,8 +1439,8 @@
   Literal integers in ML text are forced to be of this one true
   integer type --- adhoc overloading of SML97 is disabled.
 
-  Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
-  @{ML_struct Int}.  Structure @{ML_struct Integer} in @{file
+  Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
+  @{ML_structure Int}.  Structure @{ML_structure Integer} in @{file
   "~~/src/Pure/General/integer.ML"} provides some additional
   operations.
 
@@ -1487,7 +1487,7 @@
 *}
 
 text {* Apart from @{ML Option.map} most other operations defined in
-  structure @{ML_struct Option} are alien to Isabelle/ML an never
+  structure @{ML_structure Option} are alien to Isabelle/ML an never
   used.  The operations shown above are defined in @{file
   "~~/src/Pure/General/basics.ML"}.  *}
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarImplementation/Prelim.thy
--- a/src/Doc/IsarImplementation/Prelim.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -709,7 +709,7 @@
   of declared type and term variable names.  Projecting a proof
   context down to a primitive name context is occasionally useful when
   invoking lower-level operations.  Regular management of ``fresh
-  variables'' is done by suitable operations of structure @{ML_struct
+  variables'' is done by suitable operations of structure @{ML_structure
   Variable}, which is also able to provide an official status of
   ``locally fixed variable'' within the logical environment (cf.\
   \secref{sec:variables}).
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarRef/Document_Preparation.thy
--- a/src/Doc/IsarRef/Document_Preparation.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -123,7 +123,8 @@
     @{antiquotation_def ML} & : & @{text antiquotation} \\
     @{antiquotation_def ML_op} & : & @{text antiquotation} \\
     @{antiquotation_def ML_type} & : & @{text antiquotation} \\
-    @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
+    @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
+    @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
     @{antiquotation_def "file"} & : & @{text antiquotation} \\
     @{antiquotation_def "url"} & : & @{text antiquotation} \\
   \end{matharray}
@@ -175,7 +176,8 @@
       @@{antiquotation ML} options @{syntax name} |
       @@{antiquotation ML_op} options @{syntax name} |
       @@{antiquotation ML_type} options @{syntax name} |
-      @@{antiquotation ML_struct} options @{syntax name} |
+      @@{antiquotation ML_structure} options @{syntax name} |
+      @@{antiquotation ML_functor} options @{syntax name} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name}
@@ -263,9 +265,9 @@
   ``@{text _}'' placeholders there.
   
   \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
-  s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value,
-  infix operator, type, and structure, respectively.  The source is
-  printed verbatim.
+  s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"}
+  check text @{text s} as ML value, infix operator, type, structure,
+  and functor respectively.  The source is printed verbatim.
 
   \item @{text "@{file path}"} checks that @{text "path"} refers to a
   file (or directory) and prints it verbatim.
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -926,7 +926,7 @@
   defines a proof method in the current theory.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
-  basic parsers defined in structure @{ML_struct Args} and @{ML_struct
+  basic parsers defined in structure @{ML_structure Args} and @{ML_structure
   Attrib}.  There are also combinators like @{ML METHOD} and @{ML
   SIMPLE_METHOD} to turn certain tactic forms into official proof
   methods; the primed versions refer to tactics with explicit goal
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -1059,7 +1059,7 @@
   defines an attribute in the current theory.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
-  structure @{ML_struct Args} and @{ML_struct Attrib}.
+  structure @{ML_structure Args} and @{ML_structure Attrib}.
 
   In principle, attributes can operate both on a given theorem and the
   implicit context, although in practice only one is modified and the
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/LaTeXsugar/Sugar.thy
--- a/src/Doc/LaTeXsugar/Sugar.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/LaTeXsugar/Sugar.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -398,7 +398,7 @@
 
 Further use cases can be found in \S\ref{sec:yourself}.
 If you are not afraid of ML, you may also define your own styles.
-Have a look at module @{ML_struct Term_Style}.
+Have a look at module @{ML_structure Term_Style}.
 
 
 \section {Proofs}
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -64,8 +64,8 @@
       ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
         toks2 @ ml_toks ") option];";
 
-fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
-  | ml_exn (toks1, toks2) =
+fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
+  | ml_exception (toks1, toks2) =
       ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
 
 fun ml_structure (toks, _) =
@@ -121,8 +121,8 @@
   index_ml @{binding index_ML} "" ml_val #>
   index_ml @{binding index_ML_op} "infix" ml_op #>
   index_ml @{binding index_ML_type} "type" ml_type #>
-  index_ml @{binding index_ML_exn} "exception" ml_exn #>
-  index_ml @{binding index_ML_struct} "structure" ml_structure #>
+  index_ml @{binding index_ML_exception} "exception" ml_exception #>
+  index_ml @{binding index_ML_structure} "structure" ml_structure #>
   index_ml @{binding index_ML_functor} "functor" ml_functor;
 
 end;
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -25,7 +25,8 @@
 | "num_size (CN n c a) = 4 + num_size a"
 | "num_size (Mul c a) = 1 + num_size a"
 
-primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
+primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
+where
   "Inum bs (C c) = c"
 | "Inum bs (Bound n) = bs!n"
 | "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
@@ -267,15 +268,18 @@
 | "isatom p = False"
 
 lemma numsubst0_numbound0:
-  assumes nb: "numbound0 t"
+  assumes "numbound0 t"
   shows "numbound0 (numsubst0 t a)"
-  using nb apply (induct a)
+  using assms
+  apply (induct a)
   apply simp_all
-  apply (case_tac nat, simp_all)
+  apply (case_tac nat)
+  apply simp_all
   done
 
 lemma subst0_bound0:
-  assumes qf: "qfree p" and nb: "numbound0 t"
+  assumes qf: "qfree p"
+    and nb: "numbound0 t"
   shows "bound0 (subst0 t p)"
   using qf numsubst0_numbound0[OF nb] by (induct p) auto
 
@@ -356,22 +360,28 @@
   assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
   shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
 proof clarify
-  fix p assume qf: "qfree p"
-  have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
+  fix p
+  assume qf: "qfree p"
+  have th: "DJ f p = evaldjf f (disjuncts p)"
+    by (simp add: DJ_def)
   from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
-  with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast
-
-  from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
+  with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)"
+    by blast
+  from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
+    by simp
 qed
 
 lemma DJ_qe:
   assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
 proof clarify
-  fix p :: fm and bs
+  fix p :: fm
+  fix bs
   assume qf: "qfree p"
-  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast
-  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
+  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
+    by blast
+  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)"
+    by auto
   have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
     by (simp add: DJ_def evaldjf_ex)
   also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"
@@ -399,9 +409,9 @@
 
 fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
 where
-  "lex_ns [] ms = True"
-| "lex_ns ns [] = False"
-| "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
+  "lex_ns [] ms \<longleftrightarrow> True"
+| "lex_ns ns [] \<longleftrightarrow> False"
+| "lex_ns (n # ns) (m # ms) \<longleftrightarrow> n < m \<or> (n = m \<and> lex_ns ns ms)"
 
 definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
   where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
@@ -440,10 +450,12 @@
 
 lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   apply (induct t s rule: numadd.induct, simp_all add: Let_def)
-  apply (case_tac "c1 + c2 = 0", case_tac "n1 \<le> n2", simp_all)
+  apply (case_tac "c1 + c2 = 0")
+  apply (case_tac "n1 \<le> n2")
+  apply simp_all
    apply (case_tac "n1 = n2")
-    apply(simp_all add: algebra_simps)
-  apply(simp add: distrib_right[symmetric])
+    apply (simp_all add: algebra_simps)
+  apply (simp add: distrib_right[symmetric])
   done
 
 lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
@@ -452,7 +464,7 @@
 fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
 where
   "nummul i (C j) = C (i * j)"
-| "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
+| "nummul i (CN n c t) = CN n (c * i) (nummul i t)"
 | "nummul i t = Mul i t"
 
 lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
@@ -513,10 +525,14 @@
 
 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   where
-    "conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
+    "conj p q =
+      (if p = F \<or> q = F then F
+       else if p = T then q
+       else if q = T then p
+       else And p q)"
 
 lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
-  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
+  by (cases "p = F \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
 
 lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
   using conj_def by auto
@@ -527,35 +543,42 @@
 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   where
     "disj p q =
-      (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
+      (if p = T \<or> q = T then T
+       else if p = F then q
+       else if q = F then p
+       else Or p q)"
 
 lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
   by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all)
 
-lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
+lemma disj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
   using disj_def by auto
 
-lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
+lemma disj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
   using disj_def by auto
 
 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   where
-    "imp p q = (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
+    "imp p q =
+      (if p = F \<or> q = T then T
+       else if p = T then q
+       else if q = F then not p
+       else Imp p q)"
 
 lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
-  by (cases "p=F \<or> q=T", simp_all add: imp_def, cases p) (simp_all add: not)
+  by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not)
 
 lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
-  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf)
+  using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not_qf)
 
 lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
-  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
+  using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) simp_all
 
 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   where
     "iff p q =
-      (if (p = q) then T
-       else if (p = not q \<or> not p = q) then F
+      (if p = q then T
+       else if p = not q \<or> not p = q then F
        else if p = F then not q
        else if q = F then not p
        else if p = T then q
@@ -598,7 +621,7 @@
 termination by (relation "measure fmsize") auto
 
 lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
-proof(induct p rule: simpfm.induct)
+proof (induct p rule: simpfm.induct)
   case (6 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
@@ -793,48 +816,70 @@
   shows "\<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)
-  case (1 c n a) thus ?case by auto
+  case (1 c n a)
+  then show ?case by auto
 next
-  case (2 m n a) thus ?case by (cases "m=0") auto
+  case (2 m n a)
+  then show ?case by (cases "m = 0") auto
 next
   case (3 m i a n a')
   let ?j = "fst (zsplit0 a)"
   let ?b = "snd (zsplit0 a)"
-  have abj: "zsplit0 a = (?j,?b)" by simp
-  {assume "m\<noteq>0"
-    with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
+  have abj: "zsplit0 a = (?j, ?b)" by simp
+  {
+    assume "m \<noteq> 0"
+    with 3(1)[OF abj] 3(2) have ?case
+      by (auto simp add: Let_def split_def)
+  }
   moreover
-  {assume m0: "m =0"
+  {
+    assume m0: "m = 0"
     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)" by simp
-    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
-  finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
-  with th2 th have ?case using m0 by blast}
-ultimately show ?case by blast
+    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)"
+      by simp
+    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
+      by (simp add: distrib_right)
+    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)"
+      using th2 by simp
+    with th2 th have ?case using m0
+      by blast
+  }
+  ultimately show ?case by blast
 next
   case (4 t n a)
   let ?nt = "fst (zsplit0 t)"
   let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp hence 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
-  from th2[simplified] th[simplified] show ?case by simp
+  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
+  from th2[simplified] th[simplified] show ?case
+    by simp
 next
   case (5 s t n a)
   let ?ns = "fst (zsplit0 s)"
   let ?as = "snd (zsplit0 s)"
   let ?nt = "fst (zsplit0 t)"
   let ?at = "snd (zsplit0 t)"
-  have abjs: "zsplit0 s = (?ns,?as)" by simp
-  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
-  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" 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)" by auto
-  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  have abjs: "zsplit0 s = (?ns, ?as)"
+    by simp
+  moreover have abjt: "zsplit0 t = (?nt, ?at)"
+    by simp
+  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"
+    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)"
+    by auto
+  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
+    by blast
+  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
+    by blast
   from th3[simplified] th2[simplified] th[simplified] show ?case
     by (simp add: distrib_right)
 next
@@ -843,29 +888,39 @@
   let ?as = "snd (zsplit0 s)"
   let ?nt = "fst (zsplit0 t)"
   let ?at = "snd (zsplit0 t)"
-  have abjs: "zsplit0 s = (?ns,?as)" by simp
-  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
-  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" by blast
+  have abjs: "zsplit0 s = (?ns, ?as)"
+    by simp
+  moreover have abjt: "zsplit0 t = (?nt, ?at)"
+    by simp
+  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"
+    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)"
     by auto
-  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
+    by blast
+  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
+    by blast
   from th3[simplified] th2[simplified] th[simplified] show ?case
     by (simp add: left_diff_distrib)
 next
   case (7 i t n a)
   let ?nt = "fst (zsplit0 t)"
   let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp
-  hence 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
-  hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
-  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
-  finally show ?case using th th2 by simp
+  have abj: "zsplit0 t = (?nt,?at)"
+    by simp
+  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
+  then have "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)"
+    by simp
+  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))"
+    by (simp add: distrib_left)
+  finally show ?case using th th2
+    by simp
 qed
 
 consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
@@ -949,137 +1004,203 @@
   case (5 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r", auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (6 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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 6 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r", auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (7 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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 7 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r", auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (8 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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 8 Ia nb  show ?case
+  from 8 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r", auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (9 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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 9 Ia nb  show ?case
+  from 9 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r", auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (10 a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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 10 Ia nb  show ?case
+  from 10 Ia nb show ?case
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
-    apply (case_tac nat, auto)
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
     done
 next
   case (11 j a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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"
-  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
+  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" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
-    hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
+  {
+    assume "j = 0"
+    then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
+      by (simp add: Let_def)
+    then have ?case using 11 `j = 0`
+      by (simp del: zlfm.simps)
+  }
   moreover
-  {assume "?c=0" and "j\<noteq>0" hence ?case
+  {
+    assume "?c = 0" and "j \<noteq> 0"
+    then have ?case
       using zsplit0_I[OF spl, where x="i" and bs="bs"]
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
-    apply (case_tac nat, auto)
-    done}
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
+    done
+  }
   moreover
-  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+  {
+    assume cp: "?c > 0" and jnz: "j \<noteq> 0"
+    then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
+    then have ?case
+      using Ia cp jnz by (simp add: Let_def split_def)
+  }
   moreover
-  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+  { 
+    assume cn: "?c < 0" and jnz: "j \<noteq> 0"
+    then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
-      by (simp add: Let_def split_def) }
+    then have ?case
+      using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
+      by (simp add: Let_def split_def)
+  }
   ultimately show ?case by blast
 next
   case (12 j a)
   let ?c = "fst (zsplit0 a)"
   let ?r = "snd (zsplit0 a)"
-  have spl: "zsplit0 a = (?c,?r)" by simp
+  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" by auto
+  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"
-  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
+  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" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
-    hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
+  {
+    assume "j = 0"
+    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)
+  }
   moreover
-  {assume "?c=0" and "j\<noteq>0" hence ?case
+  {
+    assume "?c = 0" and "j \<noteq> 0"
+    then have ?case
       using zsplit0_I[OF spl, where x="i" and bs="bs"]
     apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
-    apply (case_tac nat, auto)
-    done}
+    apply (cases "?r")
+    apply auto
+    apply (case_tac nat)
+    apply auto
+    done
+  }
   moreover
-  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+  {
+    assume cp: "?c > 0" and jnz: "j \<noteq> 0"
+    then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
+    then have ?case using Ia cp jnz
+      by (simp add: Let_def split_def)
+  }
   moreover
-  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
+  {
+    assume cn: "?c < 0" and jnz: "j \<noteq> 0"
+    then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
-      by (simp add: Let_def split_def)}
+    then have ?case
+      using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
+      by (simp add: Let_def split_def)
+  }
   ultimately show ?case by blast
 qed auto
 
@@ -1133,10 +1254,12 @@
   shows "d_\<delta> p d'"
   using lin ad d
 proof (induct p rule: iszlfm.induct)
-  case (9 i c e)  thus ?case using d
+  case (9 i c e)
+  then show ?case using d
     by (simp add: dvd_trans[of "i" "d" "d'"])
 next
-  case (10 i c e) thus ?case using d
+  case (10 i c e)
+  then show ?case using d
     by (simp add: dvd_trans[of "i" "d" "d'"])
 qed simp_all
 
@@ -1147,21 +1270,33 @@
 proof (induct p rule: iszlfm.induct)
   case (1 p q)
   let ?d = "\<delta> (And p q)"
-  from 1 lcm_pos_int have dp: "?d >0" by simp
-  have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
-  hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
-  have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
-  hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
-  from th th' dp show ?case by simp
+  from 1 lcm_pos_int have dp: "?d > 0"
+    by simp
+  have d1: "\<delta> p dvd \<delta> (And p q)"
+    using 1 by simp
+  then have th: "d_\<delta> p ?d"
+    using delta_mono 1(2,3) by (simp only: iszlfm.simps)
+  have "\<delta> q dvd \<delta> (And p q)"
+    using 1 by simp
+  then have th': "d_\<delta> q ?d"
+    using delta_mono 1 by (simp only: iszlfm.simps)
+  from th th' dp show ?case
+    by simp
 next
   case (2 p q)
   let ?d = "\<delta> (And p q)"
-  from 2 lcm_pos_int have dp: "?d >0" by simp
-  have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
-  hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
-  have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
-  hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
-  from th th' dp show ?case by simp
+  from 2 lcm_pos_int have dp: "?d > 0"
+    by simp
+  have "\<delta> p dvd \<delta> (And p q)"
+    using 2 by simp
+  then have th: "d_\<delta> p ?d"
+    using delta_mono 2 by (simp only: iszlfm.simps)
+  have "\<delta> q dvd \<delta> (And p q)"
+    using 2 by simp
+  then have th': "d_\<delta> q ?d"
+    using delta_mono 2 by (simp only: iszlfm.simps)
+  from th th' dp show ?case
+    by simp
 qed simp_all
 
 
@@ -1247,7 +1382,9 @@
 
 text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
 
-lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
+lemma dvd1_eq1:
+  fixes x :: int
+  shows "x > 0 \<Longrightarrow> x dvd 1 \<longleftrightarrow> x = 1"
   by simp
 
 lemma minusinf_inf:
@@ -1257,25 +1394,32 @@
   (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) thus ?case
+  case (1 p q)
+  then show ?case
     by auto (rule_tac x="min z za" in exI,simp)
 next
-  case (2 p q) thus ?case
+  case (2 p q)
+  then show ?case
     by auto (rule_tac x="min z za" in exI,simp)
 next
-  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (3 c e)
+  then have c1: "c = 1" and nb: "numbound0 e"
+    by simp_all
   fix a
-  from 3 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"
+  from 3 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"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
-    show "False" by simp
+    show False by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 next
-  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (4 c e)
+  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"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -325,7 +325,7 @@
 
 ML_file "langford.ML"
 method_setup dlo = {*
-  Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+  Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
 *} "Langford's algorithm for quantifier elimination in dense linear orders"
 
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -2,13 +2,13 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
-signature LANGFORD_QE =
+signature LANGFORD =
 sig
   val dlo_tac : Proof.context -> int -> tactic
   val dlo_conv : Proof.context -> cterm -> thm
 end
 
-structure LangfordQE: LANGFORD_QE =
+structure Langford: LANGFORD =
 struct
 
 val dest_set =
@@ -21,7 +21,7 @@
 
 fun prove_finite cT u =
   let
-    val [th0, th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
+    val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
     fun ins x th =
       Thm.implies_elim
         (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
@@ -33,176 +33,195 @@
       (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
- case term_of ep of
-  Const(@{const_name Ex},_)$_ =>
-   let
-     val p = Thm.dest_arg ep
-     val ths =
-      simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (instantiate' [] [SOME p] stupid)
-     val (L,U) =
-       let
-         val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
-       in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
-       end
-     fun proveneF S =
-       let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
-           val cT = ctyp_of_term a
-           val ne = instantiate' [SOME cT] [SOME a, SOME A]
-                    @{thm insert_not_empty}
-           val f = prove_finite cT (dest_set S)
-       in (ne, f) end
+  (case term_of ep of
+    Const (@{const_name Ex}, _) $ _ =>
+      let
+        val p = Thm.dest_arg ep
+        val ths =
+          simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
+            (instantiate' [] [SOME p] stupid)
+        val (L, U) =
+          let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
+          in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
+        fun proveneF S =
+          let
+            val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
+            val cT = ctyp_of_term a
+            val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
+            val f = prove_finite cT (dest_set S)
+         in (ne, f) end
 
-     val qe = case (term_of L, term_of U) of
-      (Const (@{const_name Orderings.bot}, _),_) =>
-        let
-          val (neU,fU) = proveneF U
-        in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
-    | (_,Const (@{const_name Orderings.bot}, _)) =>
-        let
-          val (neL,fL) = proveneF L
-        in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
-
-    | (_,_) =>
-      let
-       val (neL,fL) = proveneF L
-       val (neU,fU) = proveneF U
-      in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
-      end
-   in qe end
- | _ => error "dlo_qe : Not an existential formula";
+        val qe =
+          (case (term_of L, term_of U) of
+            (Const (@{const_name Orderings.bot}, _),_) =>
+              let val (neU, fU) = proveneF U
+              in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
+          | (_, Const (@{const_name Orderings.bot}, _)) =>
+              let val (neL,fL) = proveneF L
+              in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
+          | _ =>
+              let
+                val (neL, fL) = proveneF L
+                val (neU, fU) = proveneF U
+              in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end)
+      in qe end
+  | _ => error "dlo_qe : Not an existential formula");
 
 val all_conjuncts =
- let fun h acc ct =
-  case term_of ct of
-   @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
-  | _ => ct::acc
-in h [] end;
+  let
+    fun h acc ct =
+      (case term_of ct of
+        @{term HOL.conj} $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+      | _ => ct :: acc)
+  in h [] end;
 
 fun conjuncts ct =
- case term_of ct of
-  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+  (case term_of ct of
+    @{term HOL.conj} $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
+  | _ => [ct]);
 
-fun fold1 f = foldr1 (uncurry f);
+fun fold1 f = foldr1 (uncurry f);  (* FIXME !? *)
 
-val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
+val list_conj =
+  fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c');
 
 fun mk_conj_tab th =
- let fun h acc th =
-   case prop_of th of
-   @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
-     h (h acc (th RS conjunct2)) (th RS conjunct1)
-  | @{term "Trueprop"}$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+  let
+    fun h acc th =
+      (case prop_of th of
+        @{term "Trueprop"} $ (@{term HOL.conj} $ p $ q) =>
+          h (h acc (th RS conjunct2)) (th RS conjunct1)
+      | @{term "Trueprop"} $ p => (p, th) :: acc)
+  in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
 fun is_conj (@{term HOL.conj}$_$_) = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs =
- case cjs of
-   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
- | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
+  (case cjs of
+    [c] =>
+      if is_conj (term_of c)
+      then prove_conj tab (conjuncts c)
+      else tab c
+  | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]);
 
 fun conj_aci_rule eq =
- let
-  val (l,r) = Thm.dest_equals eq
-  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
-  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
-  val ll = Thm.dest_arg l
-  val rr = Thm.dest_arg r
+  let
+    val (l, r) = Thm.dest_equals eq
+    fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
+    fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
+    val ll = Thm.dest_arg l
+    val rr = Thm.dest_arg r
+    val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
+    val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
+    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
+  in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
 
-  val thl  = prove_conj tabl (conjuncts rr)
-                |> Drule.implies_intr_hyps
-  val thr  = prove_conj tabr (conjuncts ll)
-                |> Drule.implies_intr_hyps
-  val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
- in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
+fun contains x ct =
+  member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
 
-fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
-
-fun is_eqx x eq = case term_of eq of
-   Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
- | _ => false ;
+fun is_eqx x eq =
+  (case term_of eq of
+    Const (@{const_name HOL.eq}, _) $ l $ r =>
+      l aconv term_of x orelse r aconv term_of x
+  | _ => false);
 
 local
+
 fun proc ctxt ct =
- case term_of ct of
-  Const(@{const_name Ex},_)$Abs (xn,_,_) =>
-   let
-    val e = Thm.dest_fun ct
-    val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
-    val Pp = Thm.apply @{cterm "Trueprop"} p
-    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
-   in case eqs of
-      [] =>
-        let
-         val (dx,ndx) = List.partition (contains x) neqs
-         in case ndx of [] => NONE
-                      | _ =>
-            conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
-                 (Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
-           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
-           |> Conv.fconv_rule (Conv.arg_conv
-               (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
-           |> SOME
-          end
-    | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
-                 (Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
-           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
-           |> Conv.fconv_rule (Conv.arg_conv
-               (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
-           |> SOME
-   end
- | _ => NONE;
-in val reduce_ex_simproc =
+  (case term_of ct of
+    Const (@{const_name Ex}, _) $ Abs (xn, _, _) =>
+      let
+        val e = Thm.dest_fun ct
+        val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
+        val Pp = Thm.apply @{cterm Trueprop} p
+        val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
+      in
+        (case eqs of
+          [] =>
+            let
+              val (dx, ndx) = List.partition (contains x) neqs
+            in
+              case ndx of
+                [] => NONE
+              | _ =>
+                conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+                  (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx))))
+                |> Thm.abstract_rule xn x
+                |> Drule.arg_cong_rule e
+                |> Conv.fconv_rule
+                  (Conv.arg_conv
+                    (Simplifier.rewrite
+                      (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+                |> SOME
+            end
+        | _ =>
+            conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+              (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs))))
+            |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
+            |> Conv.fconv_rule
+                (Conv.arg_conv
+                  (Simplifier.rewrite
+                    (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+            |> SOME)
+      end
+  | _ => NONE);
+
+in
+
+val reduce_ex_simproc =
   Simplifier.make_simproc
-  {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
-   proc = K proc, identifier = []}
+    {lhss = [@{cpat "\<exists>x. ?P x"}],
+     name = "reduce_ex_simproc",
+     proc = K proc,
+     identifier = []};
+
 end;
 
 fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
- let
-  val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
-  val dnfex_conv = Simplifier.rewrite ctxt'
-  val pcv =
-    Simplifier.rewrite
-      (put_simpset dlo_ss ctxt
-        addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
- in fn p =>
-   Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
-                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
-                  (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
- end;
-
+  let
+    val ctxt' =
+      Context_Position.set_visible false (put_simpset dlo_ss ctxt)
+        addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+    val dnfex_conv = Simplifier.rewrite ctxt'
+    val pcv =
+      Simplifier.rewrite
+        (put_simpset dlo_ss ctxt
+          addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
+  in
+    fn p =>
+      Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
+        (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+        (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
+  end;
 
 val grab_atom_bop =
- let
-  fun h bounds tm =
-   (case term_of tm of
-     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
-       if domain_type T = HOLogic.boolT then find_args bounds tm
-       else Thm.dest_fun2 tm
-   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
-   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
-   | Const ("==>", _) $ _ $ _ => find_args bounds tm
-   | Const ("==", _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
-   | _ => Thm.dest_fun2 tm)
-  and find_args bounds tm =
-    (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
- and find_body bounds b =
-   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
-   in h (bounds + 1) b' end;
-in h end;
+  let
+    fun h bounds tm =
+      (case term_of tm of
+        Const (@{const_name HOL.eq}, T) $ _ $ _ =>
+          if domain_type T = HOLogic.boolT then find_args bounds tm
+          else Thm.dest_fun2 tm
+      | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+      | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+      | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
+      | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+      | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+      | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+      | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
+      | Const ("==>", _) $ _ $ _ => find_args bounds tm
+      | Const ("==", _) $ _ $ _ => find_args bounds tm
+      | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
+      | _ => Thm.dest_fun2 tm)
+    and find_args bounds tm =
+      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
+    and find_body bounds b =
+      let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+      in h (bounds + 1) b' end;
+  in h end;
 
 fun dlo_instance ctxt tm =
-  (fst (Langford_Data.get ctxt),
-   Langford_Data.match ctxt (grab_atom_bop 0 tm));
+  (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
 
 fun dlo_conv ctxt tm =
   (case dlo_instance ctxt tm of
@@ -210,28 +229,28 @@
   | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
 
 fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
- let
-   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
-   fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
-   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
-   val p' = fold_rev gen ts p
- in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
-
+  let
+    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+    fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
+    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
+    val p' = fold_rev gen ts p
+  in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
 fun cfrees ats ct =
- let
-  val ins = insert (op aconvc)
-  fun h acc t =
-   case (term_of t) of
-    _$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t)
-                then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
-                else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
-  | Free _ => if member (op aconvc) ats t then acc else ins t acc
-  | Var _ => if member (op aconvc) ats t then acc else ins t acc
-  | _ => acc
- in h [] ct end
+  let
+    val ins = insert (op aconvc)
+    fun h acc t =
+      (case (term_of t) of
+        _ $ _ $ _ =>
+          if member (op aconvc) ats (Thm.dest_fun2 t)
+          then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
+          else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+      | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+      | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+      | Free _ => if member (op aconvc) ats t then acc else ins t acc
+      | Var _ => if member (op aconvc) ats t then acc else ins t acc
+      | _ => acc)
+  in h [] ct end
 
 fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   (case dlo_instance ctxt p of
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/HOL/ex/ML.thy	Sun Mar 02 22:43:20 2014 +0100
@@ -104,7 +104,7 @@
 *}
 
 text {*
-  The @{ML_struct Par_List} module provides high-level combinators for
+  The @{ML_structure Par_List} module provides high-level combinators for
   parallel list operations. *}
 
 ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/General/completion.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -9,6 +9,7 @@
   type T
   val names: Position.T -> (string * string) list -> T
   val none: T
+  val reported_text: T -> string
   val report: T -> unit
 end;
 
@@ -30,15 +31,17 @@
 
 val none = names Position.none [];
 
-fun report completion =
+fun reported_text completion =
   let val {pos, total, names} = dest completion in
     if Position.is_reported pos andalso not (null names) then
       let
         val markup = Position.markup pos Markup.completion;
         val body = (total, names) |>
           let open XML.Encode in pair int (list (pair string string)) end;
-      in Output.report (YXML.string_of (XML.Elem (markup, body))) end
-    else ()
+      in YXML.string_of (XML.Elem (markup, body)) end
+    else ""
   end;
 
+val report = Output.report o reported_text;
+
 end;
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -206,11 +206,12 @@
   if Context_Position.is_visible_generic context andalso Position.is_reported pos
   then
     let
+      val x = Name.clean xname;
       val Name_Space {kind = k, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val names =
         Symtab.fold
-          (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
+          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end
@@ -451,8 +452,9 @@
        (Context_Position.report_generic context pos (markup space name);
         (name, x))
     | NONE =>
-       (Completion.report (completion context space (xname, pos));
-        error (undefined (kind_of space) name ^ Position.here pos)))
+        error (undefined (kind_of space) name ^ Position.here pos ^
+          Markup.markup Markup.report
+            (Completion.reported_text (completion context space (xname, pos)))))
   end;
 
 fun get (space, tab) name =
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -377,11 +377,17 @@
 fun read_class ctxt text =
   let
     val tsig = tsig_of ctxt;
-    val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-    val c = Type.cert_class tsig (Type.intern_class tsig s)
-      handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
-    val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
-  in c end;
+    val class_space = Type.class_space tsig;
+
+    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    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))));
+    val _ = Context_Position.report ctxt pos (Name_Space.markup class_space name);
+  in name end;
 
 
 (* types *)
@@ -435,26 +441,7 @@
   in (xs ~~ Ts, ctxt') end;
 
 
-(* type and 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 =>
-          Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
-      | NONE => Consts.read_const consts (c, pos));
-    val _ =
-      if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
-      else ();
-    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
-  in t end;
-
-in
+(* type names *)
 
 fun read_type_name ctxt strict text =
   let
@@ -466,15 +453,13 @@
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
-        val d = intern_type ctxt c;
-        val decl = Type.the_decl tsig (d, pos);
+        val (d, decl) = Type.check_decl (Context.Proof ctxt) tsig (c, pos);
         fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
         val args =
           (case decl of
             Type.LogicalType n => n
           | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
           | Type.Nonterminal => if strict then err () else 0);
-        val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
       in Type (d, replicate args dummyT) end
   end;
 
@@ -484,6 +469,30 @@
   | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
 
 
+(* 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;
+
+in
+
 fun read_const_proper ctxt strict =
   prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -64,7 +64,7 @@
       | reported loc (PolyML.PTopenedAt decl) =
           cons (reported_entity Markup.ML_openN loc decl)
       | reported loc (PolyML.PTstructureAt decl) =
-          cons (reported_entity Markup.ML_structN loc decl)
+          cons (reported_entity Markup.ML_structureN loc decl)
       | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
       | reported _ _ = I
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -92,7 +92,7 @@
   val ML_commentN: string val ML_comment: T
   val ML_defN: string
   val ML_openN: string
-  val ML_structN: string
+  val ML_structureN: string
   val ML_typingN: string val ML_typing: T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
@@ -391,7 +391,7 @@
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
+val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 02 22:43:20 2014 +0100
@@ -204,7 +204,7 @@
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
-  val ML_STRUCT = "ML_struct"
+  val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -661,7 +661,7 @@
  (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
   ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
   ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
-  ml_text (Binding.name "ML_struct")
+  ml_text (Binding.name "ML_structure")
     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
   ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/consts.ML	Sun Mar 02 22:43:20 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 read_const: T -> string * Position.T -> term
+  val check_const: Context.generic -> T -> xstring * Position.T -> term
   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
@@ -141,11 +141,12 @@
   | NONE => s);
 
 
-(* read_const *)
+(* check_const *)
 
-fun read_const consts (raw_c, pos) =
+fun check_const context consts (xname, pos) =
   let
-    val c = intern consts raw_c;
+    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;
 
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Pure/type.ML	Sun Mar 02 22:43:20 2014 +0100
@@ -52,6 +52,7 @@
   val intern_type: tsig -> xstring -> string
   val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
+  val check_decl: Context.generic -> tsig -> xstring * Position.T -> string * decl
   val the_decl: tsig -> string * Position.T -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
@@ -257,6 +258,8 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
+fun check_decl context (TSig {types, ...}) = Name_Space.check context types;
+
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of
     NONE => error (undecl_type c ^ Position.here pos)
diff -r 8093590e49e4 -r 3a2ad5ccc1c8 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Mar 02 19:15:23 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Mar 02 22:43:20 2014 +0100
@@ -359,7 +359,7 @@
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
             { case (Markup.KIND, Markup.ML_OPEN) => true
-              case (Markup.KIND, Markup.ML_STRUCT) => true
+              case (Markup.KIND, Markup.ML_STRUCTURE) => true
               case _ => false }) =>
 
             val opt_link =