1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jun 12 14:29:10 2021 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jun 12 18:06:27 2021 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4  
     1.5  ML \<open>
     1.6    val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls
     1.7 -    [ Rule.Thm  ("rule3",ThmC.numerals_to_Free @{thm rule3}),
     1.8 -      Rule.Thm  ("rule4",ThmC.numerals_to_Free @{thm rule4}),
     1.9 -      Rule.Thm  ("rule1",ThmC.numerals_to_Free @{thm rule1})   
    1.10 +    [ \<^rule_thm>\<open>rule3\<close>,
    1.11 +      \<^rule_thm>\<open>rule4\<close>,
    1.12 +      \<^rule_thm>\<open>rule1\<close>   
    1.13      ];
    1.14  
    1.15  \<close> ML \<open>