test/Tools/isac/ProgLang/rewrite.sml
changeset 52105 2786cc9704c8
parent 52101 c3f399ce32af
child 59110 57739650f9b4
     1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Sep 16 11:28:43 2013 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Sep 16 12:20:00 2013 +0200
     1.3 @@ -370,7 +370,7 @@
     1.4  if ([], true) = eval__true thy 0 asms [] erls
     1.5  then () else error "rewrite.sml: prepat cancel eval__true";
     1.6  
     1.7 -"===== Rational.thy: common_nominator_p ===";
     1.8 +"===== Rational.thy: add_fractions_p ===";
     1.9  (* if each pat* matches with the current term, the Rrls is applied
    1.10     (there are no preconditions to be checked, they are @{term True}) *)
    1.11  val t = str2term "a / b + 1 / 2";
    1.12 @@ -382,7 +382,7 @@
    1.13  
    1.14  val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
    1.15  if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
    1.16 -then () else error "rewrite.sml: prepat common_nominator_p";
    1.17 +then () else error "rewrite.sml: prepat add_fractions_p";
    1.18  
    1.19  "===== Poly.thy: order_mult_ ===";
    1.20            (* ?p matched with the current term gives an environment,