1.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -32,5 +32,20 @@
     1.4  end
     1.5  \<close> ML \<open>
     1.6  \<close> ML \<open>
     1.7 +\<close> ML \<open>
     1.8 +fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
     1.9 +    let
    1.10 +      val tid = HOLogic.dest_string thmID
    1.11 +      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
    1.12 +    in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
    1.13 +  | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
    1.14 +     (Tactic.Rewrite_Set (HOLogic.dest_string rls))
    1.15 +  | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
    1.16 +    let
    1.17 +      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
    1.18 +    in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
    1.19 +\<close> ML \<open>
    1.20 +\<close> ML \<open>
    1.21 +\<close> ML \<open>
    1.22  \<close>
    1.23  end