1.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Thu Oct 20 12:12:18 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Fri Oct 21 15:19:00 2022 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  "table of contents -----------------------------------------------------------------------------";
     1.5  "-----------------------------------------------------------------------------------------------";
     1.6  "-----------------------------------------------------------------------------------------------";
     1.7 -"----------- fun result, fun creates_assms ---------------------------------------------------";
     1.8 +"----------- fun result, fun creates_assms -----------------------------------------------------";
     1.9 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
    1.10  "-----------------------------------------------------------------------------------------------";
    1.11  "-----------------------------------------------------------------------------------------------";
    1.12  "-----------------------------------------------------------------------------------------------";
    1.13 @@ -23,3 +24,14 @@
    1.14  ;
    1.15  if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
    1.16  if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
    1.17 +
    1.18 +
    1.19 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
    1.20 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
    1.21 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
    1.22 +val subs = ["(''bdv'', x)"];
    1.23 +
    1.24 +val [((Free ("bdv", T1)), Free ("x", T2))] = subst_adapt_to_type ctxt subs;
    1.25 +if T1 = HOLogic.realT andalso T2 = HOLogic.realT
    1.26 +then () else error "subst_adapt_to_type CHANGED";
    1.27 +