1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -41,8 +41,6 @@
     1.4  (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
     1.5  
     1.6  ML \<open>
     1.7 -val thy = @{theory};
     1.8 -
     1.9  (** eval functions **)
    1.10  
    1.11  val c = Free ("c", HOLogic.realT);