diff -r 2654f8196c36 -r 9f927860d907 src/Tools/isac/Interpret/Interpret.thy
--- a/src/Tools/isac/Interpret/Interpret.thy	Sat Apr 03 15:27:52 2021 +0200
+++ b/src/Tools/isac/Interpret/Interpret.thy	Sun Apr 04 12:29:42 2021 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory Interpret
-imports "~~/src/Tools/isac/Specify/Specify"
+imports Specify.Specify
 begin
 (* removed all warnings here, only "handle _" remains *)
   ML_file istate.sml
@@ -21,13 +21,15 @@
 
 ML \<open>
 local
-  val all_thys = @{theory} :: Theory.ancestors_of @{theory}
-  val session_interpret_names = map Context.theory_name 
-    (take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) all_thys), all_thys))
+  val thys_known_sofar = @{theory} :: Theory.ancestors_of @{theory}
+  val isac_thys_known_sofar = take (
+    find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,
+    thys_known_sofar)
+  val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar
 in
-  val check_interpret_thys =
-    if session_interpret_names = ThyC.session_interpret_names then ()
-    else raise ERROR "determine ThyC.session_interpret_names from HERE"
+  val compare_dependencies__ThyC =
+    if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
+    else raise ERROR "theory dependencies not as anticipated in ThyC"
 end
 \<close> ML \<open>
 \<close> ML \<open>