diff -r 74965ce81297 -r 844610c5c943 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Apr 29 14:13:11 2021 +0200
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Apr 29 17:02:10 2021 +0200
@@ -438,13 +438,12 @@
       eval_factors_from_solution ""))*)
       
   fun eval_factors_from_solution (thmid:string) _
-       (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
-         thy = ((let val prod = factors_from_solution sol
-                   in SOME (mk_thmid thmid "" (UnparseC.term_in_thy thy prod) "",
-                         Trueprop $ (mk_equality (t, prod)))
-                end)
-               handle _ => NONE)
-   | eval_factors_from_solution _ _ _ _ = NONE;
+      (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
+        let val prod = factors_from_solution sol
+        in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
+             HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
+        end
+    | eval_factors_from_solution _ _ _ _ = NONE;
 \<close>
 
 text \<open>\noindent The tracing output of the calc tree after applying this