1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -98,11 +98,12 @@
     1.4  "----------- Widerspruch 3 = 777 ---------------------------------";
     1.5  "----------- Widerspruch 3 = 777 ---------------------------------";
     1.6  val thy = @{theory "Isac_Knowledge"}; 
     1.7 +val ctxt = Proof_Context.init_global thy;
     1.8  val rew_ord = dummy_ord;
     1.9  val erls = Rule_Set.Empty;
    1.10  val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
    1.11  val t = TermC.str2term "0 = (0::real)";
    1.12 -val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
    1.13 +val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t;
    1.14  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
    1.15  
    1.16  val sube = ["?a1 = (3::real)"];