1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4    found in ~~/src/Tools/isac/Knowledge/Diff.thy:
     1.5  \<close>
     1.6  ML \<open>
     1.7 -val diff_sum = TermC.num_str @{thm diff_sum};
     1.8 -val diff_pow = TermC.num_str @{thm diff_pow};
     1.9 -val diff_var = TermC.num_str @{thm diff_var};
    1.10 -val diff_const = TermC.num_str @{thm diff_const};
    1.11 +val diff_sum = ThmC.numerals_to_Free @{thm diff_sum};
    1.12 +val diff_pow = ThmC.numerals_to_Free @{thm diff_pow};
    1.13 +val diff_var = ThmC.numerals_to_Free @{thm diff_var};
    1.14 +val diff_const = ThmC.numerals_to_Free @{thm diff_const};
    1.15  \<close>
    1.16  text \<open>Looking at the rules (abbreviated by 'thm' above), we see the 
    1.17    differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound