# HG changeset patch
# User nipkow
# Date 1241762825 -7200
# Node ID 9950ca962e2077e6310c679a91f3303c16df358a
# Parent  fd7ec31f850cce843722f0afeb9bc16a6a8ef91c# Parent  28dd6fd3d1840745c3573610db8b5798784906c2
merged

diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Int.thy	Fri May 08 08:07:05 2009 +0200
@@ -15,6 +15,9 @@
   "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
   "~~/src/Provers/Arith/combine_numerals.ML"
+  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+  "~~/src/Provers/Arith/extract_common_term.ML"
+  ("Tools/int_factor_simprocs.ML")
   ("Tools/int_arith.ML")
 begin
 
@@ -1517,10 +1520,11 @@
 
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
+use "Tools/int_factor_simprocs.ML"
 
 setup {*
   ReorientProc.add
-    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+    (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
 *}
 
 simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/IntDiv.thy	Fri May 08 08:07:05 2009 +0200
@@ -8,10 +8,6 @@
 
 theory IntDiv
 imports Int Divides FunDef
-uses
-  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
-  "~~/src/Provers/Arith/extract_common_term.ML"
-  ("Tools/int_factor_simprocs.ML")
 begin
 
 definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -724,7 +720,6 @@
       apply (auto simp add: divmod_rel_def) 
       apply (auto simp add: algebra_simps)
       apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
-      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
       done
     moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
     ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
@@ -1078,8 +1073,6 @@
    prefer 2
    apply (blast intro: order_less_trans)
   apply (simp add: zero_less_mult_iff)
-  apply (subgoal_tac "n * k < n * 1")
-   apply (drule mult_less_cancel_left [THEN iffD1], auto)
   done
 
 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
@@ -1334,11 +1327,6 @@
 qed
 
 
-subsection {* Simproc setup *}
-
-use "Tools/int_factor_simprocs.ML"
-
-
 subsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri May 08 08:07:05 2009 +0200
@@ -342,6 +342,7 @@
   Library/Random.thy Library/Quickcheck.thy	\
   Library/Poly_Deriv.thy \
   Library/Polynomial.thy \
+  Library/Preorder.thy \
   Library/Product_plus.thy \
   Library/Product_Vector.thy \
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Library/Library.thy	Fri May 08 08:07:05 2009 +0200
@@ -42,6 +42,7 @@
   Pocklington
   Poly_Deriv
   Polynomial
+  Preorder
   Primes
   Product_Vector
   Quickcheck
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/Library/Preorder.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Preorder.thy	Fri May 08 08:07:05 2009 +0200
@@ -0,0 +1,65 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Preorders with explicit equivalence relation *}
+
+theory Preorder
+imports Orderings
+begin
+
+class preorder_equiv = preorder
+begin
+
+definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
+
+notation
+  equiv ("op ~~") and
+  equiv ("(_/ ~~ _)" [51, 51] 50)
+  
+notation (xsymbols)
+  equiv ("op \<approx>") and
+  equiv ("(_/ \<approx> _)"  [51, 51] 50)
+
+notation (HTML output)
+  equiv ("op \<approx>") and
+  equiv ("(_/ \<approx> _)"  [51, 51] 50)
+
+lemma refl [iff]:
+  "x \<approx> x"
+  unfolding equiv_def by simp
+
+lemma trans:
+  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+  unfolding equiv_def by (auto intro: order_trans)
+
+lemma antisym:
+  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+  unfolding equiv_def ..
+
+lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
+  by (auto simp add: equiv_def less_le_not_le)
+
+lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
+  by (auto simp add: equiv_def less_le)
+
+lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
+  by (simp add: less_le)
+
+lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
+  by (simp add: less_le)
+
+lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
+  by (simp add: equiv_def less_le)
+
+lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
+  by (simp add: less_le)
+
+lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
+  by (simp add: less_le)
+
+lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
+  by (simp add: equiv_def)
+
+end
+
+end
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri May 08 08:07:05 2009 +0200
@@ -222,7 +222,7 @@
     simplify_one ss (([th, cancel_th]) MRS trans);
 
 local
-  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+  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
@@ -297,7 +297,7 @@
  (open CancelFactorCommon
   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 dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
   val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
 );
 
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Fri May 08 08:07:05 2009 +0200
@@ -4,7 +4,9 @@
 
 header {* Arithmetic *}
 
-theory Arith_Examples imports Main begin
+theory Arith_Examples
+imports Main
+begin
 
 text {*
   The @{text arith} method is used frequently throughout the Isabelle
@@ -35,87 +37,87 @@
            @{term Divides.div} *}
 
 lemma "(i::nat) <= max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::int) <= max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min i j <= (i::nat)"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min i j <= (i::int)"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min (i::nat) j <= max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min (i::int) j <= max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min (i::nat) j + max i j = i + j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "min (i::int) j + max i j = i + j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::nat) < j ==> min i j < max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::int) < j ==> min i j < max i j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(0::int) <= abs i"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::int) <= abs i"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "abs (abs (i::int)) = abs i"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 text {* Also testing subgoals with bound variables. *}
 
 lemma "!!x. (x::nat) <= y ==> x - y = 0"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "!!x. (x::nat) - y = 0 ==> x <= y"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(x::int) < y ==> x - y < 0"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "nat (i + j) <= nat i + nat j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "i < j ==> nat (i - j) = 0"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::nat) mod 0 = i"
   (* FIXME: need to replace 0 by its numeral representation *)
   apply (subst nat_numeral_0_eq_0 [symmetric])
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::nat) mod 1 = 0"
   (* FIXME: need to replace 1 by its numeral representation *)
   apply (subst nat_numeral_1_eq_1 [symmetric])
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::nat) mod 42 <= 41"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::int) mod 0 = i"
   (* FIXME: need to replace 0 by its numeral representation *)
   apply (subst numeral_0_eq_0 [symmetric])
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(i::int) mod 1 = 0"
   (* FIXME: need to replace 1 by its numeral representation *)
@@ -130,70 +132,70 @@
 oops
 
 lemma "-(i::int) * 1 = 0 ==> i = 0"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 
 subsection {* Meta-Logic *}
 
 lemma "x < Suc y == x <= y"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 
 subsection {* Various Other Examples *}
 
 lemma "(x < Suc y) = (x <= y)"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) < y; y < z |] ==> x < z"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(x::nat) < y & y < z ==> x < z"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 text {* This example involves no arithmetic at all, but is solved by
   preprocessing (i.e. NNF normalization) alone. *}
 
 lemma "(P::bool) = Q ==> Q = P"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(x::nat) - 5 > y ==> y < x"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(x::nat) ~= 0 ==> 0 < x"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
-  by (tactic {* linear_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(x - y) - (x::nat) = (x - x) - y"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
   (n = n' & n' < m) | (n = m & m < n') |
@@ -218,28 +220,28 @@
 text {* Constants. *}
 
 lemma "(0::nat) < 1"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(0::int) < 1"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(47::nat) + 11 < 08 * 15"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 lemma "(47::int) + 11 < 08 * 15"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 text {* Splitting of inequalities of different type. *}
 
 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
   a + b <= nat (max (abs i) (abs j))"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 text {* Again, but different order. *}
 
 lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
   a + b <= nat (max (abs i) (abs j))"
-  by (tactic {* fast_arith_tac @{context} 1 *})
+  by linarith
 
 (*
 ML {* reset trace_arith; *}
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/BinEx.thy	Fri May 08 08:07:05 2009 +0200
@@ -712,38 +712,38 @@
 by arith
 
 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
 by arith
 
 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
 
 
 subsection{*Complex Arithmetic*}
diff -r 28dd6fd3d184 -r 9950ca962e20 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri May 08 08:07:05 2009 +0200
@@ -10,7 +10,6 @@
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-declare disj_assoc [code del]
 lemma "0 + (n::nat) = n" by normalization
 lemma "0 + Suc n = Suc n" by normalization
 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
diff -r 28dd6fd3d184 -r 9950ca962e20 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Fri May 08 08:07:05 2009 +0200
@@ -958,10 +958,7 @@
 fun eval some_target reff postproc thy t args =
   let
     val ctxt = ProofContext.init thy;
-    val _ = if null (Term.add_frees t []) then () else error ("Term "
-      ^ quote (Syntax.string_of_term_global thy t)
-      ^ " to be evaluated contains free variables");
-    fun evaluator naming program (((_, (_, ty)), _), t) deps =
+    fun evaluator naming program ((_, (_, ty)), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
           error "Term to be evaluated contains free dictionaries" else ();
diff -r 28dd6fd3d184 -r 9950ca962e20 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Fri May 08 08:07:05 2009 +0200
@@ -85,10 +85,10 @@
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory -> (sort -> sort)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
   val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -755,7 +755,7 @@
 
 (* value evaluation *)
 
-fun ensure_value thy algbr funcgr (fs, t) =
+fun ensure_value thy algbr funcgr t =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -766,7 +766,7 @@
       ##>> translate_term thy algbr funcgr NONE t
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
-    fun term_value fs (dep, (naming, program1)) =
+    fun term_value (dep, (naming, program1)) =
       let
         val Fun (_, (vs_ty, [(([], t), _)])) =
           Graph.get_node program1 Term.dummy_patternN;
@@ -774,22 +774,19 @@
         val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.subgraph (member (op =) deps_all) program2;
-      in (((naming, program3), (((vs_ty, fs), t), deps)), (dep, (naming, program2))) end;
+      in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
   in
     ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
     #> snd
-    #> fold_map (fn (v, ty) => translate_typ thy algbr funcgr ty
-         #-> (fn ty' => pair (v, ty'))) fs
-    #-> (fn fs' => term_value fs')
+    #> term_value
   end;
 
 fun base_evaluator thy evaluator algebra funcgr vs t =
   let
-    val fs = Term.add_frees t [];
-    val (((naming, program), ((((vs', ty'), fs'), t'), deps)), _) =
-      invoke_generation thy (algebra, funcgr) ensure_value (fs, t);
+    val (((naming, program), (((vs', ty'), t'), deps)), _) =
+      invoke_generation thy (algebra, funcgr) ensure_value t;
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
-  in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
+  in evaluator naming program ((vs'', (vs', ty')), t') deps end;
 
 fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
 fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
diff -r 28dd6fd3d184 -r 9950ca962e20 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Fri May 08 08:07:05 2009 +0200
@@ -293,19 +293,22 @@
 fun obtain thy cs ts = apsnd snd
   (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun prepare_sorts prep_sort (Const (c, ty)) = Const (c, map_type_tfree
-      (fn (v, sort) => TFree (v, prep_sort sort)) ty)
+fun prepare_sorts_typ prep_sort
+  = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
+
+fun prepare_sorts prep_sort (Const (c, ty)) =
+      Const (c, prepare_sorts_typ prep_sort ty)
   | prepare_sorts prep_sort (t1 $ t2) =
       prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
   | prepare_sorts prep_sort (Abs (v, ty, t)) =
-      Abs (v, Type.strip_sorts ty, prepare_sorts prep_sort t)
-  | prepare_sorts _ (Term.Free (v, ty)) = Term.Free (v, Type.strip_sorts ty)
+      Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
   | prepare_sorts _ (t as Bound _) = t;
 
 fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
   let
+    val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
-    val _ = (Term.map_types Type.no_tvars o Sign.no_vars (Syntax.pp_global thy))
+    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
       (Thm.term_of ct);
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
@@ -313,6 +316,7 @@
     val vs = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
+ 
     val t'' = prepare_sorts prep_sort t';
     val (algebra', eqngr') = obtain thy consts [t''];
   in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
diff -r 28dd6fd3d184 -r 9950ca962e20 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/nbe.ML	Fri May 08 08:07:05 2009 +0200
@@ -11,7 +11,6 @@
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
-    | Free of string * Univ list             (*free (uninterpreted) variables*)
     | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)
     | BVar of int * Univ list
     | Abs of (int * (Univ list -> Univ)) * Univ list
@@ -57,14 +56,12 @@
 
 datatype Univ =
     Const of int * Univ list           (*named (uninterpreted) constants*)
-  | Free of string * Univ list         (*free variables*)
   | DFree of string * int              (*free (uninterpreted) dictionary parameters*)
   | BVar of int * Univ list            (*bound variables, named*)
   | Abs of (int * (Univ list -> Univ)) * Univ list
                                        (*abstractions as closures*);
 
 fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
-  | same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys
   | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
   | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
   | same _ _ = false
@@ -80,7 +77,6 @@
         | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
       end
   | apps (Const (name, xs)) ys = Const (name, ys @ xs)
-  | apps (Free (name, xs)) ys = Free (name, ys @ xs)
   | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
 
 
@@ -352,14 +348,12 @@
 
 fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
   let 
-    val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
-    val frees' = map (fn v => Free (v, [])) frees;
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
-    ("", (vs, [(map IVar frees, t)]))
+    ("", (vs, [([], t)]))
     |> singleton (compile_eqnss ctxt gr deps)
     |> snd
-    |> (fn t => apps t (rev (dict_frees @ frees')))
+    |> (fn t => apps t (rev dict_frees))
   end;
 
 (* reification *)
@@ -399,8 +393,6 @@
             val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T;
             val typidx' = typidx + 1;
           in of_apps bounds (Term.Const (c, T'), ts') typidx' end
-      | of_univ bounds (Free (name, ts)) typidx =
-          of_apps bounds (Term.Free (name, dummyT), ts) typidx
       | of_univ bounds (BVar (n, ts)) typidx =
           of_apps bounds (Bound (bounds - n - 1), ts) typidx
       | of_univ bounds (t as Abs _) typidx =
@@ -440,15 +432,12 @@
 
 (* evaluation with type reconstruction *)
 
-fun normalize thy naming program (((vs0, (vs, ty)), fs), t) deps =
+fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
     val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
     val ty' = typ_of_itype program vs0 ty;
-    val fs' = (map o apsnd) (typ_of_itype program vs0) fs;
-    val type_frees = Term.map_aterms (fn (t as Term.Free (s, _)) =>
-      Term.Free (s, (the o AList.lookup (op =) fs') s) | t => t);
     fun type_infer t =
       singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
@@ -461,8 +450,6 @@
     compile_eval thy naming program (vs, t) deps
     |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
     |> resubst_triv_consts
-    |> type_frees
-    |> tracing (fn t => "Vars typed:\n" ^ string_of_term t)
     |> type_infer
     |> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
     |> check_tvars
@@ -482,18 +469,41 @@
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_fs_t, deps, ct) =>
-    mk_equals thy ct (normalize thy naming program vsp_ty_fs_t deps))));
+  (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_t, deps, ct) =>
+    mk_equals thy ct (normalize thy naming program vsp_ty_t deps))));
+
+fun norm_oracle thy naming program vsp_ty_t deps ct =
+  raw_norm_oracle (thy, naming, program, vsp_ty_t, deps, ct);
 
-fun norm_oracle thy naming program vsp_ty_fs_t deps ct =
-  raw_norm_oracle (thy, naming, program, vsp_ty_fs_t, deps, ct);
+fun no_frees_conv conv ct =
+  let
+    val frees = Thm.add_cterm_frees ct [];
+    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
+      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+  in
+    ct
+    |> fold_rev Thm.cabs frees
+    |> conv
+    |> fold apply_beta frees
+  end;
 
-fun norm_conv ct =
+fun no_frees_rew rew t =
+  let
+    val frees = map Free (Term.add_frees t []);
+  in
+    t
+    |> fold_rev lambda frees
+    |> rew
+    |> (fn t' => Term.betapplys (t', frees))
+  end;
+
+val norm_conv = no_frees_conv (fn ct =>
   let
     val thy = Thm.theory_of_cterm ct;
-  in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
+  in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end);
 
-fun norm thy = Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy);
+fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy));
 
 (* evaluation command *)