1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jul 18 21:19:25 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jul 19 15:34:54 2021 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  (*("occur_exactly_in", ("EqSystem.occur_exactly_in", 
     1.5                          eval_occur_exactly_in "#eval_occur_exactly_in_") )*)
     1.6  fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
     1.7 -			  (p as (Const ("EqSystem.occur_exactly_in",_) 
     1.8 +			  (p as (Const (\<^const_name>\<open>EqSystem.occur_exactly_in\<close>,_) 
     1.9  				       $ vs $ all $ t)) _ =
    1.10      if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
    1.11      then SOME ((UnparseC.term p) ^ " = True",