1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -287,7 +287,7 @@
     1.4  val SOME (t,_) = 
     1.5      rewrite_inst_ thy e_rew_ord 
     1.6  		  (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty 
     1.7 -			      [(Eval ("EqSystem.occur'_exactly'_in", 
     1.8 +			      [(Eval ("EqSystem.occur_exactly_in", 
     1.9  				      eval_occur_exactly_in 
    1.10  					  "#eval_occur_exactly_in_"))
    1.11  			       ]) 
    1.12 @@ -353,7 +353,7 @@
    1.13  val pres = [TermC.parse_patt thy "?p is_multUnordered"];
    1.14  val prepat = [(pres, pat)];
    1.15  val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
    1.16 -		      [Eval ("Poly.is'_multUnordered", 
    1.17 +		      [Eval ("Poly.is_multUnordered", 
    1.18                               eval_is_multUnordered "")];
    1.19  
    1.20  val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
    1.21 @@ -376,7 +376,7 @@
    1.22  case eval_is_multUnordered "testid" "" tm thy of
    1.23      SOME (_, Const ("HOL.Trueprop", _) $ 
    1.24                     (Const ("HOL.eq", _) $
    1.25 -                          (Const ("Poly.is'_multUnordered", _) $ _) $ 
    1.26 +                          (Const ("Poly.is_multUnordered", _) $ _) $ 
    1.27                            Const ("HOL.True", _))) => ()
    1.28    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.29  
    1.30 @@ -384,7 +384,7 @@
    1.31  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
    1.32  tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
    1.33  if UnparseC.term t' = "x * x \<up> 2" then ()
    1.34 -else error "rewrite.sml Poly.is'_multUnordered doesn't work";
    1.35 +else error "rewrite.sml Poly.is_multUnordered doesn't work";
    1.36  
    1.37  (* for achieving the previous result, the following code was taken apart *)
    1.38  "----- rewrite__set_ ---";
    1.39 @@ -607,7 +607,7 @@
    1.40  (*+*)    Thm ("not_false", "(\<not> False) = True"),
    1.41  (*+*)    :
    1.42  (*+*)    Eval ("Transcendental.powr", fn),
    1.43 -(*+*)    Eval ("RatEq.is'_ratequation'_in", fn)]:
    1.44 +(*+*)    Eval ("RatEq.is_ratequation_in", fn)]:
    1.45  (*+*)   rule list*)
    1.46  (*+*)chk: term list -> term list -> term list * bool
    1.47