1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sun Jul 18 21:19:25 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jul 19 15:34:54 2021 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  (*WN080222
     1.6  (*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
     1.7 -fun eval_new_c _ _ (p as (Const ("Integrate.new_c",_) $ t)) _ =
     1.8 +fun eval_new_c _ _ (p as (Const (\<^const_name>\<open>Integrate.new_c\<close>,_) $ t)) _ =
     1.9       SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
    1.10  	  Trueprop $ (mk_equality (p, new_c p)))
    1.11    | eval_new_c _ _ _ _ = NONE;
    1.12 @@ -93,7 +93,7 @@
    1.13  
    1.14  
    1.15  (*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
    1.16 -fun eval_is_f_x _ _(p as (Const ("Integrate.is_f_x", _)
    1.17 +fun eval_is_f_x _ _(p as (Const (\<^const_name>\<open>Integrate.is_f_x\<close>, _)
    1.18  					   $ arg)) _ =
    1.19      if TermC.is_f_x arg
    1.20      then SOME ((UnparseC.term p) ^ " = True",