1.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml	Sat Apr 03 15:27:52 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml	Sun Apr 04 12:29:42 2021 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val cut_id: string -> id
     1.5  
     1.6    val last_isabelle_thy: theory
     1.7 +  val session_specify_names: id list
     1.8    val session_interpret_names: id list
     1.9    val get_theory: id -> theory         (* restricted to Isac_Knowledge *)
    1.10    val id_to_ctxt: id -> Proof.context
    1.11 @@ -36,11 +37,14 @@
    1.12  fun cut_id dn = hd (space_explode "." dn);
    1.13  
    1.14  val last_isabelle_thy = @{theory Complex_Main}
    1.15 -val session_interpret_names = ["Interpret", "Specify", "MathEngBasic", "Input_Descript",
    1.16 +val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",
    1.17    "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calculate",
    1.18    "BaseDefinitions", "Know_Store"]
    1.19 +val session_interpret_names = ["Interpret"]
    1.20  fun get_thy thyID =
    1.21 -  if member op = session_interpret_names thyID
    1.22 +  if member op = session_specify_names thyID
    1.23 +  then Thy_Info.get_theory ("Specify." ^ thyID)
    1.24 +  else if member op = session_interpret_names thyID
    1.25    then Thy_Info.get_theory ("Interpret." ^ thyID)
    1.26    else Thy_Info.get_theory ("Isac." ^ thyID);
    1.27  fun get_theory thy =