1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Tue Apr 14 15:56:15 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Apr 15 10:07:43 2020 +0200
     1.3 @@ -71,11 +71,11 @@
     1.4  fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
     1.5      let
     1.6        val tid = HOLogic.dest_string thmID
     1.7 -    in (Tactic.Rewrite (tid, ThmC.assoc_thm'' thy tid)) end
     1.8 +    in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
     1.9    | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
    1.10      let
    1.11        val tid = HOLogic.dest_string thmID
    1.12 -    in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, ThmC.assoc_thm'' thy tid))) end
    1.13 +    in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, ThmC.thm_from_thy thy tid))) end
    1.14    | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
    1.15       (Tactic.Rewrite_Set (HOLogic.dest_string rls))
    1.16    | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =