test/Tools/isac/Interpret/error-pattern.sml
changeset 60594 439f7f3867ec
parent 60586 007ef64dbb08
child 60608 5dabcc1c9235
     1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Wed Nov 16 10:30:59 2022 +0100
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Wed Nov 16 17:42:41 2022 +0100
     1.3 @@ -118,13 +118,13 @@
     1.4  
     1.5   val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
     1.6  		       ((#rules o Rule_Set.rep) Test_simplify)
     1.7 -		       (sqrt_right false (@{theory "Pure"})) NONE 
     1.8 +		       (sqrt_right false) NONE 
     1.9  		       (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
    1.10   (writeln o Derive.trtas2str) fod;
    1.11  
    1.12   val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
    1.13  		       ((#rules o Rule_Set.rep) Test_simplify)
    1.14 -		       (sqrt_right false (@{theory "Pure"})) NONE 
    1.15 +		       (sqrt_right false) NONE 
    1.16  		       (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
    1.17   (writeln o Derive.trtas2str) ifod;
    1.18   fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;