1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 16 11:28:43 2013 +0200
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 16 12:20:00 2013 +0200
1.3 @@ -214,9 +214,7 @@
1.4 in scan_ chk prepat end;
1.5 (* apply the normal_form of a rev-set *)
1.6 fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
1.7 - if chk_prepat thy erls prepat t
1.8 - then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
1.9 - else NONE;
1.10 + if chk_prepat thy erls prepat t then normal_form t else NONE;
1.11 val opt = app_rev' thy rrls t
1.12 in
1.13 case opt of