1.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Sat Apr 03 15:27:52 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Sun Apr 04 12:29:42 2021 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  
     1.6  theory Interpret
     1.7 -imports "~~/src/Tools/isac/Specify/Specify"
     1.8 +imports Specify.Specify
     1.9  begin
    1.10  (* removed all warnings here, only "handle _" remains *)
    1.11    ML_file istate.sml
    1.12 @@ -21,13 +21,15 @@
    1.13  
    1.14  ML \<open>
    1.15  local
    1.16 -  val all_thys = @{theory} :: Theory.ancestors_of @{theory}
    1.17 -  val session_interpret_names = map Context.theory_name 
    1.18 -    (take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) all_thys), all_thys))
    1.19 +  val thys_known_sofar = @{theory} :: Theory.ancestors_of @{theory}
    1.20 +  val isac_thys_known_sofar = take (
    1.21 +    find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,
    1.22 +    thys_known_sofar)
    1.23 +  val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar
    1.24  in
    1.25 -  val check_interpret_thys =
    1.26 -    if session_interpret_names = ThyC.session_interpret_names then ()
    1.27 -    else raise ERROR "determine ThyC.session_interpret_names from HERE"
    1.28 +  val compare_dependencies__ThyC =
    1.29 +    if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
    1.30 +    else raise ERROR "theory dependencies not as anticipated in ThyC"
    1.31  end
    1.32  \<close> ML \<open>
    1.33  \<close> ML \<open>