merged
authorwenzelm
Sun, 22 Mar 2009 21:48:14 +0100
changeset 30651 94b74365ceb9
parent 30650 226c91456e54 (diff)
parent 30646 d26ad4576d5c (current diff)
child 30659 a400b06d03cb
merged
--- a/doc-src/IsarOverview/Isar/Induction.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -143,14 +143,14 @@
 universally quantifies all \emph{vars} before the induction.  Hence
 they can be replaced by \emph{arbitrary} values in the proof.
 
-The nice thing about generalization via @{text"arbitrary:"} is that in
-the induction step the claim is available in unquantified form but
+Generalization via @{text"arbitrary"} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
 with the generalized variables replaced by @{text"?"}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
+for instantiation. In the above example, in the @{const[source] Cons} case the
+induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available
+under the name @{const[source] Cons}).
 
-For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
-behind the scenes.
 
 \subsection{Inductive proofs of conditional formulae}
 \label{sec:full-Ind}
--- a/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -30,8 +30,8 @@
   show A by(rule a)
 qed
 
-text{*\noindent Single-identifier formulae such as @{term A} need not
-be enclosed in double quotes. However, we will continue to do so for
+text{*\noindent As you see above, single-identifier formulae such as @{term A}
+need not be enclosed in double quotes. However, we will continue to do so for
 uniformity.
 
 Instead of applying fact @{text a} via the @{text rule} method, we can
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -342,14 +342,14 @@
 universally quantifies all \emph{vars} before the induction.  Hence
 they can be replaced by \emph{arbitrary} values in the proof.
 
-The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
-the induction step the claim is available in unquantified form but
+Generalization via \isa{arbitrary} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
 with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
+for instantiation. In the above example, in the \isa{Cons} case the
+induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys} (available
+under the name \isa{Cons}).
 
-For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
-behind the scenes.
 
 \subsection{Inductive proofs of conditional formulae}
 \label{sec:full-Ind}
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -93,8 +93,8 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent Single-identifier formulae such as \isa{A} need not
-be enclosed in double quotes. However, we will continue to do so for
+\noindent As you see above, single-identifier formulae such as \isa{A}
+need not be enclosed in double quotes. However, we will continue to do so for
 uniformity.
 
 Instead of applying fact \isa{a} via the \isa{rule} method, we can
--- a/doc-src/TutorialI/Documents/Documents.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -617,7 +617,7 @@
   same types as they have in the main goal statement.
 
   \medskip Several further kinds of antiquotations and options are
-  available \cite{isabelle-sys}.  Here are a few commonly used
+  available \cite{isabelle-isar-ref}.  Here are a few commonly used
   combinations:
 
   \medskip
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -691,7 +691,7 @@
   same types as they have in the main goal statement.
 
   \medskip Several further kinds of antiquotations and options are
-  available \cite{isabelle-sys}.  Here are a few commonly used
+  available \cite{isabelle-isar-ref}.  Here are a few commonly used
   combinations:
 
   \medskip
--- a/doc-src/TutorialI/Rules/rules.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -2138,11 +2138,11 @@
 
 \index{*insert (method)|(}%
 The \isa{insert} method
-inserts a given theorem as a new assumption of the current subgoal.  This
+inserts a given theorem as a new assumption of all subgoals.  This
 already is a forward step; moreover, we may (as always when using a
 theorem) apply
 \isa{of}, \isa{THEN} and other directives.  The new assumption can then
-be used to help prove the subgoal.
+be used to help prove the subgoals.
 
 For example, consider this theorem about the divides relation.  The first
 proof step inserts the distributive law for
--- a/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -299,7 +299,7 @@
 \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
-(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
+(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{UN_iff}
 \end{isabelle}
@@ -414,12 +414,12 @@
 $k$-element subsets of~$A$ is \index{binomial coefficients}
 $\binom{n}{k}$.
 
-\begin{warn}
-The term \isa{finite\ A} is defined via a syntax translation as an
-abbreviation for \isa{A {\isasymin} Finites}, where the constant
-\cdx{Finites} denotes the set of all finite sets of a given type.  There
-is no constant \isa{finite}.
-\end{warn}
+%\begin{warn}
+%The term \isa{finite\ A} is defined via a syntax translation as an
+%abbreviation for \isa{A {\isasymin} Finites}, where the constant
+%\cdx{Finites} denotes the set of all finite sets of a given type.  There
+%is no constant \isa{finite}.
+%\end{warn}
 \index{sets|)}
 
 
--- a/doc-src/TutorialI/Types/Overloading2.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -15,7 +15,7 @@
               size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
 
 text{*\noindent
-The infix function @{text"!"} yields the nth element of a list.
+The infix function @{text"!"} yields the nth element of a list, starting with 0.
 
 \begin{warn}
 A type constructor can be instantiated in only one way to
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Sun Mar 22 21:30:21 2009 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Sun Mar 22 21:48:14 2009 +0100
@@ -46,7 +46,7 @@
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.
+The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
 
 \begin{warn}
 A type constructor can be instantiated in only one way to
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -3783,8 +3783,7 @@
     also from mult_left_mono[OF xp] np have "?N s \<le> real n * x + ?N s" by simp
     finally have "?N (Floor s) \<le> real n * x + ?N s" .
     moreover
-    {from mult_strict_left_mono[OF x1] np 
-      have "real n *x + ?N s < real n + ?N s" by simp
+    {from x1 np have "real n *x + ?N s < real n + ?N s" by simp
       also from real_of_int_floor_add_one_gt[where r="?N s"] 
       have "\<dots> < real n + ?N (Floor s) + 1" by simp
       finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp}
@@ -3809,8 +3808,7 @@
     moreover from mult_left_mono_neg[OF xp] nn have "?N s \<ge> real n * x + ?N s" by simp
     ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith 
     moreover
-    {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
-      have "real n *x + ?N s \<ge> real n + ?N s" by simp 
+    {from x1 nn have "real n *x + ?N s \<ge> real n + ?N s" by simp
       moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
       ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
 	by (simp only: algebra_simps)}
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -1494,8 +1494,7 @@
     have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
       using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
     also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
-      using th1 th0 `e>0` apply auto
-      unfolding mult_assoc and real_mult_le_cancel_iff2[OF `e>0`] by auto
+      using th1 th0 `e>0` by auto
 
     finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
       using thx and e by (simp add: field_simps)  }
@@ -3558,7 +3557,7 @@
     { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
       hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
 	using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
-	  mult_less_imp_less_left[of "abs c" "norm ((1 / c) *s y - x)" e, unfolded real_mult_commute[of "abs c" e]] assms(1)[unfolded zero_less_abs_iff[THEN sym]] by simp
+	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
       hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"]  e[THEN spec[where x="(1 / c) *s y"]]  assms(1) unfolding dist_def vector_smult_assoc by auto  }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto  }
   thus ?thesis unfolding open_def by auto
--- a/src/HOL/Rational.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Rational.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -691,7 +691,6 @@
     \<longleftrightarrow> Fract a b < Fract c d"
     using not_zero `b * d > 0`
     by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
-      (auto intro: mult_strict_right_mono mult_right_less_imp_less)
 qed
 
 lemma of_rat_less_eq:
--- a/src/HOL/Ring_and_Field.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -1136,6 +1136,27 @@
   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
 
+lemma mult_le_cancel_left_pos:
+  "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
+by (auto simp: mult_le_cancel_left)
+
+lemma mult_le_cancel_left_neg:
+  "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
+by (auto simp: mult_le_cancel_left)
+
+end
+
+context ordered_ring_strict
+begin
+
+lemma mult_less_cancel_left_pos:
+  "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
+by (auto simp: mult_less_cancel_left)
+
+lemma mult_less_cancel_left_neg:
+  "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
+by (auto simp: mult_less_cancel_left)
+
 end
 
 text{*Legacy - use @{text algebra_simps} *}
--- a/src/HOL/Series.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Series.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -557,7 +557,6 @@
 apply (induct_tac "na", auto)
 apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
 apply (auto intro: mult_right_mono simp add: summable_def)
-apply (simp add: mult_ac)
 apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
 apply (rule sums_divide) 
 apply (rule sums_mult)
--- a/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -218,9 +218,30 @@
 val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
 
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
     simplify_one ss (([th, cancel_th]) MRS trans);
 
+local
+  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+  fun Eq_True_elim Eq = 
+    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
+in
+fun sign_conv pos_th neg_th ss t =
+  let val T = fastype_of t;
+      val zero = Const(@{const_name HOL.zero}, T);
+      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+      val pos = less $ zero $ t and neg = less $ t $ zero
+      fun prove p =
+        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+        handle THM _ => NONE
+    in case prove pos of
+         SOME th => SOME(th RS pos_th)
+       | NONE => (case prove neg of
+                    SOME th => SOME(th RS neg_th)
+                  | NONE => NONE)
+    end;
+end
+
 structure CancelFactorCommon =
   struct
   val mk_sum            = long_mk_prod
@@ -231,6 +252,7 @@
   val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+  val simplify_meta_eq  = cancel_simplify_meta_eq 
   end;
 
 (*mult_cancel_left requires a ring with no zero divisors.*)
@@ -239,7 +261,27 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
+  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+);
+
+(*for ordered rings*)
+structure LeCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Arith_Data.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+  val simp_conv = sign_conv
+    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
+);
+
+(*for ordered rings*)
+structure LessCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Arith_Data.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+  val simp_conv = sign_conv
+    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
 );
 
 (*zdiv_zmult_zmult1_if is for integer division (div).*)
@@ -248,7 +290,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
+  val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
 );
 
 structure IntModCancelFactor = ExtractCommonTermFun
@@ -256,7 +298,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
+  val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
 );
 
 structure IntDvdCancelFactor = ExtractCommonTermFun
@@ -264,7 +306,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
+  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
 );
 
 (*Version for all fields, including unordered ones (type complex).*)
@@ -273,7 +315,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
+  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
 );
 
 val cancel_factors =
@@ -281,7 +323,15 @@
    [("ring_eq_cancel_factor",
      ["(l::'a::{idom}) * m = n",
       "(l::'a::{idom}) = m * n"],
-    K EqCancelFactor.proc),
+     K EqCancelFactor.proc),
+    ("ordered_ring_le_cancel_factor",
+     ["(l::'a::ordered_ring) * m <= n",
+      "(l::'a::ordered_ring) <= m * n"],
+     K LeCancelFactor.proc),
+    ("ordered_ring_less_cancel_factor",
+     ["(l::'a::ordered_ring) * m < n",
+      "(l::'a::ordered_ring) < m * n"],
+     K LessCancelFactor.proc),
     ("int_div_cancel_factor",
      ["((l::int) * m) div n", "(l::int) div (m * n)"],
      K IntDivCancelFactor.proc),
--- a/src/HOL/Tools/nat_simprocs.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -352,7 +352,7 @@
 val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
 
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
     simplify_one ss (([th, cancel_th]) MRS trans);
 
 structure CancelFactorCommon =
@@ -365,6 +365,7 @@
   val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+  val simplify_meta_eq  = cancel_simplify_meta_eq
   end;
 
 structure EqCancelFactor = ExtractCommonTermFun
@@ -372,7 +373,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
+  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
 );
 
 structure LessCancelFactor = ExtractCommonTermFun
@@ -380,7 +381,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
+  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
@@ -388,7 +389,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
+  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
 );
 
 structure DivideCancelFactor = ExtractCommonTermFun
@@ -396,7 +397,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
+  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
 );
 
 structure DvdCancelFactor = ExtractCommonTermFun
@@ -404,7 +405,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
+  val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
 );
 
 val cancel_factor =
--- a/src/HOL/Word/WordArith.thy	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/HOL/Word/WordArith.thy	Sun Mar 22 21:48:14 2009 +0100
@@ -701,6 +701,7 @@
   apply (erule (2) udvd_decr0)
   done
 
+ML{*Delsimprocs cancel_factors*}
 lemma udvd_incr2_K: 
   "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
     0 < K ==> p <= p + K & p + K <= a + s"
@@ -716,6 +717,7 @@
    apply arith
   apply simp
   done
+ML{*Delsimprocs cancel_factors*}
 
 (* links with rbl operations *)
 lemma word_succ_rbl:
--- a/src/Provers/Arith/extract_common_term.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Provers/Arith/extract_common_term.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -25,7 +25,8 @@
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val norm_tac: simpset -> tactic                (*proves the result*)
-  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the result*)
+  val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
+  val simp_conv: simpset -> term -> thm option  (*proves simp thm*)
 end;
 
 
@@ -58,6 +59,9 @@
     and terms2 = Data.dest_sum t2
 
     val u = find_common (terms1,terms2)
+    val simp_th =
+          case Data.simp_conv ss u of NONE => raise TERM("no simp", [])
+          | SOME th => th
     val terms1' = Data.find_first u terms1
     and terms2' = Data.find_first u terms2
     and T = Term.fastype_of u
@@ -66,7 +70,7 @@
       Data.prove_conv [Data.norm_tac ss] ctxt prems
         (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
   in
-    Option.map (export o Data.simplify_meta_eq ss) reshape
+    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE
--- a/src/Pure/General/table.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Pure/General/table.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -383,3 +383,6 @@
 
 structure Inttab = TableFun(type key = int val ord = int_ord);
 structure Symtab = TableFun(type key = string val ord = fast_string_ord);
+structure Symreltab = TableFun(type key = string * string
+  val ord = prod_ord fast_string_ord fast_string_ord);
+
--- a/src/Tools/code/code_haskell.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_haskell.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -42,18 +42,18 @@
      of [] => []
       | classbinds => Pretty.enum "," "(" ")" (
           map (fn (v, class) =>
-            str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
+            str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
           @@ str " => ";
     fun pr_typforall tyvars vs = case map fst vs
      of [] => []
       | vnames => str "forall " :: Pretty.breaks
-          (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+          (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
     fun pr_tycoexpr tyvars fxy (tyco, tys) =
       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
          of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
           | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
-      | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
+      | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
     fun pr_typdecl tyvars (vs, tycoexpr) =
       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
     fun pr_typscheme tyvars (vs, ty) =
@@ -69,7 +69,7 @@
                   pr_term tyvars thm vars BR t2
                 ])
       | pr_term tyvars thm vars fxy (IVar v) =
-          (str o Code_Name.lookup_var vars) v
+          (str o Code_Printer.lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = Code_Thingol.unfold_abs t;
@@ -127,7 +127,7 @@
       | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
           let
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             val n = (length o fst o Code_Thingol.unfold_fun) ty;
           in
             Pretty.chunks [
@@ -150,7 +150,7 @@
       | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
           let
             val eqs = filter (snd o snd) raw_eqs;
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_eq ((ts, t), (thm, _)) =
               let
                 val consts = map_filter
@@ -158,8 +158,8 @@
                     then NONE else (SOME o Long_Name.base_name o deresolve) c)
                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                 val vars = init_syms
-                  |> Code_Name.intro_vars consts
-                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                  |> Code_Printer.intro_vars consts
+                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                        (insert (op =)) ts []);
               in
                 semicolon (
@@ -182,7 +182,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
           let
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
           in
             semicolon [
               str "data",
@@ -191,7 +191,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
           let
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
           in
             semicolon (
               str "newtype"
@@ -204,7 +204,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
           let
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_co (co, tys) =
               concat (
                 (str o deresolve_base) co
@@ -222,7 +222,7 @@
           end
       | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
           let
-            val tyvars = Code_Name.intro_vars [v] init_syms;
+            val tyvars = Code_Printer.intro_vars [v] init_syms;
             fun pr_classparam (classparam, ty) =
               semicolon [
                 (str o deresolve_base) classparam,
@@ -234,7 +234,7 @@
               Pretty.block [
                 str "class ",
                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
-                str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
+                str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
                 str " where {"
               ],
               str "};"
@@ -244,7 +244,7 @@
           let
             val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
             val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
-            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
                     (str o deresolve_base) classparam,
@@ -259,8 +259,8 @@
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
                     val (vs, rhs) = unfold_abs_pure proto_rhs;
                     val vars = init_syms
-                      |> Code_Name.intro_vars (the_list const)
-                      |> Code_Name.intro_vars vs;
+                      |> Code_Printer.intro_vars (the_list const)
+                      |> Code_Printer.intro_vars vs;
                     val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage*)
                   in
@@ -288,20 +288,20 @@
   let
     val module_alias = if is_some module_name then K module_name else raw_module_alias;
     val reserved_names = Name.make_context reserved_names;
-    val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
+    val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
     fun add_stmt (name, (stmt, deps)) =
       let
-        val (module_name, base) = Code_Name.dest_name name;
+        val (module_name, base) = Code_Printer.dest_name name;
         val module_name' = mk_name_module module_name;
         val mk_name_stmt = yield_singleton Name.variants;
         fun add_fun upper (nsp_fun, nsp_typ) =
           let
             val (base', nsp_fun') =
-              mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
+              mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
           in (base', (nsp_fun', nsp_typ)) end;
         fun add_typ (nsp_fun, nsp_typ) =
           let
-            val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
+            val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
           in (base', (nsp_fun, nsp_typ')) end;
         val add_name = case stmt
          of Code_Thingol.Fun _ => add_fun false
@@ -330,7 +330,7 @@
       (Graph.get_node program name, Graph.imm_succs program name))
       (Graph.strong_conn program |> flat)) Symtab.empty;
     fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
-      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
+      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
@@ -357,7 +357,7 @@
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    val reserved_names = Code_Name.make_vars reserved_names;
+    val reserved_names = Code_Printer.make_vars reserved_names;
     fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
       syntax_class syntax_tyco syntax_const reserved_names
       (if qualified then deresolver else Long_Name.base_name o deresolver)
--- a/src/Tools/code/code_ml.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_ml.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -50,8 +50,8 @@
     val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
     fun pr_dicts fxy ds =
       let
-        fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
-          | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
+        fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
+          | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
         fun pr_proj [] p =
               p
           | pr_proj [p'] p =
@@ -87,7 +87,7 @@
     fun pr_term is_closure thm vars fxy (IConst c) =
           pr_app is_closure thm vars fxy (c, [])
       | pr_term is_closure thm vars fxy (IVar v) =
-          str (Code_Name.lookup_var vars v)
+          str (Code_Printer.lookup_var vars v)
       | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -182,7 +182,7 @@
                 then NONE else (SOME o Long_Name.base_name o deresolve) c)
                 (Code_Thingol.fold_constnames (insert (op =)) t []);
             val vars = reserved_names
-              |> Code_Name.intro_vars consts;
+              |> Code_Printer.intro_vars consts;
           in
             concat [
               str "val",
@@ -207,8 +207,8 @@
                         then NONE else (SOME o Long_Name.base_name o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                     val vars = reserved_names
-                      |> Code_Name.intro_vars consts
-                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                            (insert (op =)) ts []);
                   in
                     concat (
@@ -266,7 +266,7 @@
           in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = Code_Name.first_upper v ^ "_";
+            val w = Code_Printer.first_upper v ^ "_";
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
@@ -362,8 +362,8 @@
   let
     fun pr_dicts fxy ds =
       let
-        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
-          | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
+        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
+          | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
         fun pr_proj ps p =
           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
         fun pr_dict fxy (DictConst (inst, dss)) =
@@ -395,7 +395,7 @@
     fun pr_term is_closure thm vars fxy (IConst c) =
           pr_app is_closure thm vars fxy (c, [])
       | pr_term is_closure thm vars fxy (IVar v) =
-          str (Code_Name.lookup_var vars v)
+          str (Code_Printer.lookup_var vars v)
       | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -468,8 +468,8 @@
         val x = Name.variant (map_filter I fished1) "x";
         val fished2 = map_index (fillup_param x) fished1;
         val (fished3, _) = Name.variants fished2 Name.context;
-        val vars' = Code_Name.intro_vars fished3 vars;
-      in map (Code_Name.lookup_var vars') fished3 end;
+        val vars' = Code_Printer.intro_vars fished3 vars;
+      in map (Code_Printer.lookup_var vars') fished3 end;
     fun pr_stmt (MLExc (name, n)) =
           let
             val exc_str =
@@ -491,7 +491,7 @@
                 then NONE else (SOME o Long_Name.base_name o deresolve) c)
                 (Code_Thingol.fold_constnames (insert (op =)) t []);
             val vars = reserved_names
-              |> Code_Name.intro_vars consts;
+              |> Code_Printer.intro_vars consts;
           in
             concat [
               str "let",
@@ -511,8 +511,8 @@
                     then NONE else (SOME o Long_Name.base_name o deresolve) c)
                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                 val vars = reserved_names
-                  |> Code_Name.intro_vars consts
-                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                  |> Code_Printer.intro_vars consts
+                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas)
@@ -527,8 +527,8 @@
                         then NONE else (SOME o Long_Name.base_name o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                     val vars = reserved_names
-                      |> Code_Name.intro_vars consts
-                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (
@@ -556,7 +556,7 @@
                         ((fold o Code_Thingol.fold_constnames)
                           (insert (op =)) (map (snd o fst) eqs) []);
                     val vars = reserved_names
-                      |> Code_Name.intro_vars consts;
+                      |> Code_Printer.intro_vars consts;
                     val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
@@ -623,7 +623,7 @@
           in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = "_" ^ Code_Name.first_upper v;
+            val w = "_" ^ Code_Printer.first_upper v;
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 deresolve classrel, ":", "'" ^ v, deresolve class
@@ -765,11 +765,11 @@
       let
         val (x, nsp_typ') = f nsp_typ
       in (x, (nsp_fun, nsp_typ')) end;
-    val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
+    val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
     fun mk_name_stmt upper name nsp =
       let
-        val (_, base) = Code_Name.dest_name name;
-        val base' = if upper then Code_Name.first_upper base else base;
+        val (_, base) = Code_Printer.dest_name name;
+        val base' = if upper then Code_Printer.first_upper base else base;
         val ([base''], nsp') = Name.variants [base'] nsp;
       in (base'', nsp') end;
     fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
@@ -853,7 +853,7 @@
           []
           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
           |> subtract (op =) names;
-        val (module_names, _) = (split_list o map Code_Name.dest_name) names;
+        val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
           handle Empty =>
             error ("Different namespace prefixes for mutual dependencies:\n"
@@ -863,7 +863,7 @@
         val module_name_path = Long_Name.explode module_name;
         fun add_dep name name' =
           let
-            val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
+            val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
           in if module_name = module_name' then
             map_node module_name_path (Graph.add_edge (name, name'))
           else let
@@ -891,7 +891,7 @@
           (rev (Graph.strong_conn program)));
     fun deresolver prefix name = 
       let
-        val module_name = (fst o Code_Name.dest_name) name;
+        val module_name = (fst o Code_Printer.dest_name) name;
         val module_name' = (Long_Name.explode o mk_name_module) module_name;
         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
         val stmt_name =
@@ -914,7 +914,7 @@
     val module_name = if null stmt_names then raw_module_name else SOME "Code";
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
       reserved_names raw_module_alias program;
-    val reserved_names = Code_Name.make_vars reserved_names;
+    val reserved_names = Code_Printer.make_vars reserved_names;
     fun pr_node prefix (Dummy _) =
           NONE
       | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
--- a/src/Tools/code/code_name.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_name.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -6,45 +6,20 @@
 
 signature CODE_NAME =
 sig
-  structure StringPairTab: TABLE
-  val first_upper: string -> string
-  val first_lower: string -> string
-  val dest_name: string -> string * string
-
   val purify_var: string -> string
   val purify_tvar: string -> string
-  val purify_sym: string -> string
-  val purify_base: bool -> string -> string
+  val purify_base: string -> string
   val check_modulename: string -> string
 
-  type var_ctxt
-  val make_vars: string list -> var_ctxt
-  val intro_vars: string list -> var_ctxt -> var_ctxt
-  val lookup_var: var_ctxt -> string -> string
-
   val read_const_exprs: theory -> string list -> string list * string list
-  val mk_name_module: Name.context -> string option -> (string -> string option)
-    -> 'a Graph.T -> string -> string
 end;
 
 structure Code_Name: CODE_NAME =
 struct
 
-(** auxiliary **)
-
-structure StringPairTab =
-  TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
-  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-
 (** purification **)
 
-fun purify_name upper lower =
+fun purify_name upper =
   let
     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
     val is_junk = not o is_valid andf Symbol.is_regular;
@@ -55,9 +30,8 @@
         --| junk))
       ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
-      else if lower then (if forall Symbol.is_ascii_upper cs
-        then map else nth_map 0) Symbol.to_ascii_lower cs
-      else cs;
+      else (if forall Symbol.is_ascii_upper cs
+        then map else nth_map 0) Symbol.to_ascii_lower cs;
   in
     explode
     #> scan_valids
@@ -68,7 +42,7 @@
   end;
 
 fun purify_var "" = "x"
-  | purify_var v = purify_name false true v;
+  | purify_var v = purify_name false v;
 
 fun purify_tvar "" = "'a"
   | purify_tvar v =
@@ -81,52 +55,29 @@
       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   #> implode
   #> Long_Name.explode
-  #> map (purify_name true false);
+  #> map (purify_name true);
 
 (*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base _ "op &" = "and"
-  | purify_base _ "op |" = "or"
-  | purify_base _ "op -->" = "implies"
-  | purify_base _ "{}" = "empty"
-  | purify_base _ "op :" = "member"
-  | purify_base _ "op Int" = "intersect"
-  | purify_base _ "op Un" = "union"
-  | purify_base _ "*" = "product"
-  | purify_base _ "+" = "sum"
-  | purify_base lower s = if String.isPrefix "op =" s
-      then "eq" ^ purify_name false lower s
-      else purify_name false lower s;
-
-val purify_sym = purify_base false;
+fun purify_base "op &" = "and"
+  | purify_base "op |" = "or"
+  | purify_base "op -->" = "implies"
+  | purify_base "op :" = "member"
+  | purify_base "*" = "product"
+  | purify_base "+" = "sum"
+  | purify_base s = if String.isPrefix "op =" s
+      then "eq" ^ purify_name false s
+      else purify_name false s;
 
 fun check_modulename mn =
   let
     val mns = Long_Name.explode mn;
-    val mns' = map (purify_name true false) mns;
+    val mns' = map (purify_name true) mns;
   in
     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
       ^ "perhaps try " ^ quote (Long_Name.implode mns'))
   end;
 
 
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
-  Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
-  let
-    val (names', namectxt') = Name.variants names namectxt;
-    val namemap' = fold2 (curry Symtab.update) names names' namemap;
-  in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
-  | NONE => error ("Invalid name in context: " ^ quote name);
-
-
 (** misc **)
 
 fun read_const_exprs thy =
@@ -150,22 +101,4 @@
           else ([Code_Unit.read_const thy s], []);
   in pairself flat o split_list o map read_const_expr end;
 
-fun mk_name_module reserved_names module_prefix module_alias program =
-  let
-    fun mk_alias name = case module_alias name
-     of SOME name' => name'
-      | NONE => name
-          |> Long_Name.explode
-          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
-          |> Long_Name.implode;
-    fun mk_prefix name = case module_prefix
-     of SOME module_prefix => Long_Name.append module_prefix name
-      | NONE => name;
-    val tab =
-      Symtab.empty
-      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
-           o fst o dest_name o fst)
-             program
-  in the o Symtab.lookup tab end;
-
 end;
--- a/src/Tools/code/code_printer.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_printer.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -16,6 +16,13 @@
   val semicolon: Pretty.T list -> Pretty.T
   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
 
+  val first_upper: string -> string
+  val first_lower: string -> string
+  type var_ctxt
+  val make_vars: string list -> var_ctxt
+  val intro_vars: string list -> var_ctxt -> var_ctxt
+  val lookup_var: var_ctxt -> string -> string
+
   type lrx
   val L: lrx
   val R: lrx
@@ -42,14 +49,14 @@
     -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
   val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
     -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
-  val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
-    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+  val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
+    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option) -> Code_Thingol.naming
-    -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
+    -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
-    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
+    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
 
   type literals
   val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -60,6 +67,10 @@
   val literal_numeral: literals -> bool -> int -> string
   val literal_list: literals -> Pretty.T list -> Pretty.T
   val infix_cons: literals -> int * string
+
+  val mk_name_module: Name.context -> string option -> (string -> string option)
+    -> 'a Graph.T -> string -> string
+  val dest_name: string -> string * string
 end;
 
 structure Code_Printer : CODE_PRINTER =
@@ -83,6 +94,27 @@
   | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
 
 
+(** names and variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
+
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+  Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
+  let
+    val (names', namectxt') = Name.variants names namectxt;
+    val namemap' = fold2 (curry Symtab.update) names names' namemap;
+  in (namemap', namectxt') end;
+
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+  | NONE => error ("Invalid name in context: " ^ quote name);
+
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+
+
 (** syntax printer **)
 
 (* binding priorities *)
@@ -125,8 +157,8 @@
 
 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   -> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+  -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
 fun simple_const_syntax x = (Option.map o apsnd)
   (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
@@ -150,9 +182,9 @@
     val vs = case pat
      of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
-    val vars' = Code_Name.intro_vars (the_list v) vars;
-    val vars'' = Code_Name.intro_vars vs vars';
-    val v' = Option.map (Code_Name.lookup_var vars') v;
+    val vars' = intro_vars (the_list v) vars;
+    val vars'' = intro_vars vs vars';
+    val v' = Option.map (lookup_var vars') v;
     val pat' = Option.map (pr_term thm vars'' fxy) pat;
   in (pr_bind ((v', pat'), ty), vars'') end;
 
@@ -239,4 +271,28 @@
 val literal_list = #literal_list o dest_Literals;
 val infix_cons = #infix_cons o dest_Literals;
 
+
+(** module name spaces **)
+
+val dest_name =
+  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
+
+fun mk_name_module reserved_names module_prefix module_alias program =
+  let
+    fun mk_alias name = case module_alias name
+     of SOME name' => name'
+      | NONE => name
+          |> Long_Name.explode
+          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+          |> Long_Name.implode;
+    fun mk_prefix name = case module_prefix
+     of SOME module_prefix => Long_Name.append module_prefix name
+      | NONE => name;
+    val tab =
+      Symtab.empty
+      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+           o fst o dest_name o fst)
+             program
+  in the o Symtab.lookup tab end;
+
 end; (*struct*)
--- a/src/Tools/code/code_target.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_target.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -82,11 +82,9 @@
 
 (** theory data **)
 
-structure StringPairTab = Code_Name.StringPairTab;
-
 datatype name_syntax_table = NameSyntaxTable of {
   class: string Symtab.table,
-  instance: unit StringPairTab.table,
+  instance: unit Symreltab.table,
   tyco: tyco_syntax Symtab.table,
   const: const_syntax Symtab.table
 };
@@ -99,7 +97,7 @@
     NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
   mk_name_syntax_table (
     (Symtab.join (K snd) (class1, class2),
-       StringPairTab.join (K snd) (instance1, instance2)),
+       Symreltab.join (K snd) (instance1, instance2)),
     (Symtab.join (K snd) (tyco1, tyco2),
        Symtab.join (K snd) (const1, const2))
   );
@@ -194,7 +192,7 @@
     thy
     |> (CodeTargetData.map o apfst oo Symtab.map_default)
           (target, mk_target ((serial (), seri), (([], Symtab.empty),
-            (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
+            (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
               Symtab.empty))))
           ((map_target o apfst o apsnd o K) seri)
   end;
@@ -262,11 +260,11 @@
   in if add_del then
     thy
     |> (map_name_syntax target o apfst o apsnd)
-        (StringPairTab.update (inst, ()))
+        (Symreltab.update (inst, ()))
   else
     thy
     |> (map_name_syntax target o apfst o apsnd)
-        (StringPairTab.delete_safe inst)
+        (Symreltab.delete_safe inst)
   end;
 
 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
@@ -407,7 +405,7 @@
       |>> map_filter I;
     val (names_class, class') = distill_names Code_Thingol.lookup_class class;
     val names_inst = map_filter (Code_Thingol.lookup_instance naming)
-      (StringPairTab.keys instance);
+      (Symreltab.keys instance);
     val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
     val (names_const, const') = distill_names Code_Thingol.lookup_const const;
     val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
--- a/src/Tools/code/code_thingol.ML	Sun Mar 22 21:30:21 2009 +0100
+++ b/src/Tools/code/code_thingol.ML	Sun Mar 22 21:48:14 2009 +0100
@@ -242,7 +242,7 @@
   fun namify thy get_basename get_thyname name =
     let
       val prefix = get_thyname thy name;
-      val base = (Code_Name.purify_base true o get_basename) name;
+      val base = (Code_Name.purify_base o get_basename) name;
     in Long_Name.append prefix base end;
 in
 
@@ -261,13 +261,11 @@
 
 (* data *)
 
-structure StringPairTab = Code_Name.StringPairTab;
-
 datatype naming = Naming of {
   class: class Symtab.table * Name.context,
-  classrel: string StringPairTab.table * Name.context,
+  classrel: string Symreltab.table * Name.context,
   tyco: string Symtab.table * Name.context,
-  instance: string StringPairTab.table * Name.context,
+  instance: string Symreltab.table * Name.context,
   const: string Symtab.table * Name.context
 }
 
@@ -275,9 +273,9 @@
 
 val empty_naming = Naming {
   class = (Symtab.empty, Name.context),
-  classrel = (StringPairTab.empty, Name.context),
+  classrel = (Symreltab.empty, Name.context),
   tyco = (Symtab.empty, Name.context),
-  instance = (StringPairTab.empty, Name.context),
+  instance = (Symreltab.empty, Name.context),
   const = (Symtab.empty, Name.context)
 };
 
@@ -334,22 +332,22 @@
 val lookup_class = add_suffix suffix_class
   oo Symtab.lookup o fst o #class o dest_Naming;
 val lookup_classrel = add_suffix suffix_classrel
-  oo StringPairTab.lookup o fst o #classrel o dest_Naming;
+  oo Symreltab.lookup o fst o #classrel o dest_Naming;
 val lookup_tyco = add_suffix suffix_tyco
   oo Symtab.lookup o fst o #tyco o dest_Naming;
 val lookup_instance = add_suffix suffix_instance
-  oo StringPairTab.lookup o fst o #instance o dest_Naming;
+  oo Symreltab.lookup o fst o #instance o dest_Naming;
 val lookup_const = add_suffix suffix_const
   oo Symtab.lookup o fst o #const o dest_Naming;
 
 fun declare_class thy = declare thy map_class
   lookup_class Symtab.update_new namify_class;
 fun declare_classrel thy = declare thy map_classrel
-  lookup_classrel StringPairTab.update_new namify_classrel;
+  lookup_classrel Symreltab.update_new namify_classrel;
 fun declare_tyco thy = declare thy map_tyco
   lookup_tyco Symtab.update_new namify_tyco;
 fun declare_instance thy = declare thy map_instance
-  lookup_instance StringPairTab.update_new namify_instance;
+  lookup_instance Symreltab.update_new namify_instance;
 fun declare_const thy = declare thy map_const
   lookup_const Symtab.update_new namify_const;