1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -83,8 +83,8 @@
     1.4    this is _not in_ the term, because only applied to _whole_ term*)
     1.5  fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
     1.6      let val p' = case p of
     1.7 -		     Const ("HOL.eq", T) $ lh $ rh => 
     1.8 -		     Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
     1.9 +		     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh => 
    1.10 +		     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh)
    1.11  		   | p => TermC.mk_add p (new_c p)
    1.12      in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p',
    1.13  	  HOLogic.Trueprop $ (TermC.mk_equality (p, p')))