# HG changeset patch # User krauss # Date 1288088505 -7200 # Node ID 397b791e8411990d31c19c1d334471f1c22bbfcd # Parent 97b69fef52291d9957e1e336f2441d385908d6e4# Parent 1c7e836872b08ddc948815d21ffce18cd6fd86c9 merged diff -r 97b69fef5229 -r 397b791e8411 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Oct 26 12:19:02 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Tue Oct 26 12:21:45 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)