1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -11,8 +11,6 @@
     1.4  axiomatization where
     1.5    int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     1.6  
     1.7 -ML \<open>val thy = @{theory}\<close>
     1.8 -
     1.9  text \<open>problemclass for the usecase\<close>
    1.10  setup \<open>KEStore_Elems.add_pbts
    1.11    [(Problem.prep_input @{theory} "pbl_equ_dio" [] Problem.id_empty