1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Apr 29 14:13:11 2021 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Apr 29 17:02:10 2021 +0200
     1.3 @@ -438,13 +438,12 @@
     1.4        eval_factors_from_solution ""))*)
     1.5        
     1.6    fun eval_factors_from_solution (thmid:string) _
     1.7 -       (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
     1.8 -         thy = ((let val prod = factors_from_solution sol
     1.9 -                   in SOME (mk_thmid thmid "" (UnparseC.term_in_thy thy prod) "",
    1.10 -                         Trueprop $ (mk_equality (t, prod)))
    1.11 -                end)
    1.12 -               handle _ => NONE)
    1.13 -   | eval_factors_from_solution _ _ _ _ = NONE;
    1.14 +      (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
    1.15 +        let val prod = factors_from_solution sol
    1.16 +        in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
    1.17 +             HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
    1.18 +        end
    1.19 +    | eval_factors_from_solution _ _ _ _ = NONE;
    1.20  \<close>
    1.21  
    1.22  text \<open>\noindent The tracing output of the calc tree after applying this