1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Apr 13 13:13:07 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Apr 13 13:27:55 2020 +0200
     1.3 @@ -216,7 +216,7 @@
     1.4  		      (t as Const ("Rational.get_denominator", _) $
     1.5                (Const ("Rings.divide_class.divide", _) $num 
     1.6                  $denom)) thy = 
     1.7 -        SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy denom) "", 
     1.8 +        SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", 
     1.9  	        HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
    1.10    | eval_get_denominator _ _ _ _ = NONE; 
    1.11  \<close>
    1.12 @@ -236,7 +236,7 @@
    1.13  		      (t as Const ("Rational.get_numerator", _) $
    1.14                (Const ("Rings.divide_class.divide", _) $num
    1.15                  $denom )) thy = 
    1.16 -        SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy num) "", 
    1.17 +        SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "", 
    1.18  	        HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
    1.19    | eval_get_numerator _ _ _ _ = NONE; 
    1.20  \<close>
    1.21 @@ -440,7 +440,7 @@
    1.22    fun eval_factors_from_solution (thmid:string) _
    1.23         (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
    1.24           thy = ((let val prod = factors_from_solution sol
    1.25 -                   in SOME (mk_thmid thmid "" (UnparseC.term_thy thy prod) "",
    1.26 +                   in SOME (mk_thmid thmid "" (UnparseC.term_in_thy thy prod) "",
    1.27                           Trueprop $ (mk_equality (t, prod)))
    1.28                  end)
    1.29                 handle _ => NONE)