1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4  
     1.5  ML \<open>
     1.6    val inverse_Z = Rule_Set.append_rules "inverse_Z" Rule_Set.empty
     1.7 -    [ Thm  ("rule3",TermC.num_str @{thm rule3}),
     1.8 -      Thm  ("rule4",TermC.num_str @{thm rule4}),
     1.9 -      Thm  ("rule1",TermC.num_str @{thm rule1})   
    1.10 +    [ Thm  ("rule3",ThmC.numerals_to_Free @{thm rule3}),
    1.11 +      Thm  ("rule4",ThmC.numerals_to_Free @{thm rule4}),
    1.12 +      Thm  ("rule1",ThmC.numerals_to_Free @{thm rule1})   
    1.13      ];
    1.14  
    1.15    val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
    1.16 @@ -91,19 +91,19 @@
    1.17  ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
    1.18  ML \<open>
    1.19    val SOME (t, asm1) = 
    1.20 -    Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
    1.21 +    Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule3}) t;
    1.22    UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
    1.23    (*- real *)
    1.24    UnparseC.term t;
    1.25  
    1.26    val SOME (t, asm2) = 
    1.27 -    Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule4}) t;
    1.28 +    Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
    1.29    UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
    1.30    (*- real *)
    1.31    UnparseC.term t;
    1.32  
    1.33    val SOME (t, asm3) = 
    1.34 -    Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;
    1.35 +    Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
    1.36    UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
    1.37    (*- real *)
    1.38    UnparseC.term t;
    1.39 @@ -701,8 +701,8 @@
    1.40      Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
    1.41        erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.42        rules = [
    1.43 -        Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
    1.44 -        Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
    1.45 +        Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
    1.46 +        Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
    1.47                ], 
    1.48        scr = EmptyScr});
    1.49  \<close>
    1.50 @@ -1096,9 +1096,9 @@
    1.51             ], 
    1.52           srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.53           rules = [
    1.54 -                  Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.55 +                  Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
    1.56                    Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.57 -                  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.58 +                  Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    1.59                    Num_Calc("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.60                    Num_Calc("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.61                    Num_Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),