1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Dec 31 14:49:16 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Thu Jan 10 18:17:48 2019 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4            crls = Atools_erls, errpats = [], nrls = norm_diff},
     1.5          "Script DiffScr (f_f::real) (v_v::real) =                          " ^
     1.6            " (let f_f' = Take (d_d v_v f_f)                                    " ^
     1.7 -          " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@    " ^
     1.8 +          " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@    " ^
     1.9            " (Repeat                                                        " ^
    1.10            "   ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum''        False)) Or " ^
    1.11            "    (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
    1.12 @@ -356,7 +356,7 @@
    1.13            crls=Atools_erls, errpats = [], nrls = norm_diff},
    1.14          "Script DiffEqScr (f_f::bool) (v_v::real) =                          " ^
    1.15            " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))            " ^
    1.16 -          " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@      " ^
    1.17 +          " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@      " ^
    1.18            " (Repeat                                                          " ^
    1.19            "   ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum''        False)) Or   " ^
    1.20            "    (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_dif''        False)) Or   " ^
    1.21 @@ -376,7 +376,7 @@
    1.22            "    (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const''      False)) Or   " ^
    1.23            "    (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var''        False)) Or   " ^
    1.24            "    (Repeat (Rewrite_Set                  ''make_polynomial'' False)))) @@ " ^
    1.25 -          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')          ")]
    1.26 +          " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')          ")]
    1.27  \<close>
    1.28  setup \<open>KEStore_Elems.add_mets
    1.29      [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID