1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Jan 22 11:21:08 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Jan 22 12:08:32 2019 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4             "      (facs::real) = factors_from_solution L_L;                "^
     1.5             "      (eql::real) = Take (num_orig / facs);                    "^ 
     1.6        
     1.7 -           "      (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;  "^
     1.8 +           "      (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql;  "^
     1.9        
    1.10             "      (eq::bool) = Take (eql = eqr);                           "^
    1.11             (*Maybe possible to use HOLogic.mk_eq ??*)
    1.12 @@ -152,7 +152,7 @@
    1.13         
    1.14             "      (eq_a::bool) = Take eq;                                  "^
    1.15             "      eq_a = (Substitute [zzz=z1]) eq;                         "^
    1.16 -           "      eq_a = (Rewrite_Set norm_Rational False) eq_a;           "^
    1.17 +           "      eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;           "^
    1.18             "      (sol_a::bool list) =                                     "^
    1.19             "                 (SubProblem (''Isac'',                           "^
    1.20             "                              [''univariate'',''equation''],[''no_met''])  "^