1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -298,10 +298,10 @@
     1.4    let val rew = rewrite_set_ thy false srls t;
     1.5    in case rew of SOME (res,_) => res | NONE => t end;
     1.6  
     1.7 -fun eval_true_ _ _ (Const ("HOL.True",_)) = true
     1.8 +fun eval_true_ _ _ (Const (\<^const_name>\<open>True\<close>,_)) = true
     1.9    | eval_true_ thy rls t =
    1.10      case rewrite_set_ thy false rls t of
    1.11 -	   SOME (Const ("HOL.True",_),_) => true
    1.12 +	   SOME (Const (\<^const_name>\<open>True\<close>,_),_) => true
    1.13  	 | _ => false;
    1.14  
    1.15  end