# HG changeset patch
# User haftmann
# Date 1288088168 -7200
# Node ID 1c7e836872b08ddc948815d21ffce18cd6fd86c9
# Parent  d3bc972b7d9d19fee48fca20a3967df0459eed7e# Parent  e44d0471692019b002493eea51061586b53336b3
merged

diff -r d3bc972b7d9d -r 1c7e836872b0 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:16:08 2010 +0200
@@ -480,7 +480,6 @@
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false thy consts [t'];
-    val result = evaluator algebra' eqngr' vs' t';
   in
     evaluator algebra' eqngr' vs' t'
     |> postproc (postprocess_term thy o resubst)