1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Wed Oct 10 18:41:15 2012 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Fri Oct 12 16:03:07 2012 +0200
     1.3 @@ -354,7 +354,7 @@
     1.4  "===== Rational.thy: cancel ===";
     1.5  (* pat matched with the current term gives an environment 
     1.6     (or not: hen the Rrls not applied);
     1.7 -   if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
     1.8 +   if pre1 and pre2 evaluate to @{term True} in this environment,
     1.9     then the Rrls is applied. *)
    1.10  val t = str2term "(a + b) / c ::real";
    1.11  val pat = parse_patt thy "?r / ?s ::real";
    1.12 @@ -372,10 +372,10 @@
    1.13  
    1.14  "===== Rational.thy: common_nominator_p ===";
    1.15  (* if each pat* matches with the current term, the Rrls is applied
    1.16 -   (there are no preconditions to be checked, they are HOLogic.true_const) *)
    1.17 +   (there are no preconditions to be checked, they are @{term True}) *)
    1.18  val t = str2term "a / b + 1 / 2";
    1.19  val pat = parse_patt thy "?r / ?s + ?u / ?v";
    1.20 -val pres = [HOLogic.true_const];
    1.21 +val pres = [@{term True}];
    1.22  val prepat = [(pres, pat)];
    1.23  val erls = rational_erls;
    1.24  (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)