1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -73,16 +73,19 @@
     1.4    | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
     1.5      let
     1.6        val tid = HOLogic.dest_string thmID
     1.7 -    in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
     1.8 +      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
     1.9 +    in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
    1.10    | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
    1.11       (Tactic.Rewrite_Set (HOLogic.dest_string rls))
    1.12 -  | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
    1.13 -      (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
    1.14 +  | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
    1.15 +    let
    1.16 +      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
    1.17 +    in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
    1.18    | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
    1.19        (Tactic.Calculate (HOLogic.dest_string op_))
    1.20    | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t))
    1.21 -  | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
    1.22 -    (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
    1.23 +  | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
    1.24 +      Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
    1.25    | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $ 
    1.26      (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =
    1.27        (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
    1.28 @@ -341,7 +344,7 @@
    1.29  	else ();
    1.30  (*
    1.31    check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
    1.32 -  snd of return value is the formal arguments in case of currying.
    1.33 +  snd of return value are the formal arguments in case of currying.
    1.34  *)
    1.35  fun check_leaf call ctxt srls (E, (a, v)) t =
    1.36      case Prog_Tac.eval_leaf E a v t of