1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Apr 15 16:46:41 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Apr 15 18:00:58 2020 +0200
     1.3 @@ -322,7 +322,7 @@
     1.4        (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
     1.5           AssOnly => Term_Val1 act_arg
     1.6         | _(*ORundef*) =>
     1.7 -          case Applicable.applicable_in p pt (LItool.tac_from_prog pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
     1.8 +          case Applicable.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) of
     1.9               Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
    1.10             | Applicable.Notappl _ => Term_Val1 act_arg)
    1.11