1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Mon Aug 26 09:20:07 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Mon Aug 26 17:40:27 2019 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  (*there seemed to be no way to do these tests within DiophantEq.thy:
     1.5  val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
     1.6    from CalcTreeTest*)
     1.7 -(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
     1.8 +(*val thy = @{theory "Isac_Knowledge"};toplevel error from store_met?!?*)
     1.9  *)
    1.10  val thy = @{theory "DiophantEq"};
    1.11  val ctxt = Proof_Context.init_global thy;