# HG changeset patch # User haftmann # Date 1288088371 -7200 # Node ID 30482e17955bbbf246cda1a98c1f445646e61b46 # Parent 397b791e8411990d31c19c1d334471f1c22bbfcd# Parent d88c47ca45576c46895799760beca8f1e06eb38d merged diff -r 397b791e8411 -r 30482e17955b src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Oct 26 12:21:45 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Tue Oct 26 12:19:31 2010 +0200 @@ -481,7 +481,8 @@ (fn Const (c, _) => insert (op =) c | _ => I) t' []; val (algebra', eqngr') = obtain false thy consts [t']; in - evaluator algebra' eqngr' vs' t' + t' + |> evaluator algebra' eqngr' vs' |> postproc (postprocess_term thy o resubst) end;