author | haftmann |
Tue, 26 Oct 2010 12:15:55 +0200 | |
changeset 40167 | e44d04716920 |
parent 40150 | 1348d4982a17 |
child 40168 | 1c7e836872b0 |
--- a/src/Tools/Code/code_preproc.ML Tue Oct 26 11:20:14 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Tue Oct 26 12:15:55 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)