src/Tools/isac/ProgLang/rewrite.sml
changeset 52105 2786cc9704c8
parent 52101 c3f399ce32af
child 52121 9690a8d5f1c0
     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