1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -80,9 +80,11 @@
     1.4      ];
     1.5  
     1.6  \<close> ML \<open>
     1.7 -  val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
     1.8 +  val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";
     1.9  \<close> ML \<open>
    1.10    val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
    1.11 +(*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
    1.12 +\<close> ML \<open>
    1.13    UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
    1.14    (*
    1.15     * Attention rule1 is applied before the expression is 
    1.16 @@ -216,7 +218,7 @@
    1.17   *  ("Rational.get_denominator", eval_get_denominator ""))
    1.18   *)
    1.19  fun eval_get_denominator (thmid:string) _ 
    1.20 -		      (t as Const ("Rational.get_denominator", _) $
    1.21 +		      (t as Const (\<^const_name>\<open>get_denominator\<close>, _) $
    1.22                (Const (\<^const_name>\<open>divide\<close>, _) $num 
    1.23                  $denom)) thy = 
    1.24          SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", 
    1.25 @@ -236,7 +238,7 @@
    1.26   *  ("Rational.get_numerator", eval_get_numerator ""))
    1.27   *)
    1.28  fun eval_get_numerator (thmid:string) _ 
    1.29 -		      (t as Const ("Rational.get_numerator", _) $
    1.30 +		      (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
    1.31                (Const (\<^const_name>\<open>divide\<close>, _) $num
    1.32                  $denom )) thy = 
    1.33          SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",