1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Aug 26 09:20:07 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Aug 26 17:40:27 2019 +0200
     1.3 @@ -423,16 +423,16 @@
     1.4  val erls = erls_ordne_alphabetisch;
     1.5  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
     1.6  val SOME (t',_) = 
     1.7 -    rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus} t;
     1.8 +    rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
     1.9  term2str t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
    1.10  
    1.11  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.12  val NONE = 
    1.13 -    rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
    1.14 +    rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
    1.15  
    1.16  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.17  val SOME (t',_) = 
    1.18 -    rewrite_set_ (@{theory "Isac"}) false ordne_alphabetisch t;
    1.19 +    rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
    1.20  term2str t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
    1.21  trace_rewrite := false;
    1.22