1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
     1.5    add a new c to a term or a fun-equation;
     1.6    this is _not in_ the term, because only applied to _whole_ term*)
     1.7 -fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
     1.8 +fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:Proof.context) =
     1.9      let val p' = case p of
    1.10  		     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh => 
    1.11  		     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh)