test/Tools/isac/Interpret/mathengine.sml
changeset 59262 0ddb3f300cce
parent 59253 f0bb15a046ae
child 59279 255c853ea2f0
     1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Tue Nov 22 10:42:21 2016 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Thu Nov 24 14:33:42 2016 +0100
     1.3 @@ -660,6 +660,7 @@
     1.4  val (form, tac, asms) = pt_extract (pt, p)
     1.5  val SOME ta = tac;
     1.6  "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
     1.7 +val i = 2;
     1.8  "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
     1.9  "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
    1.10  ID = "rnorm_equation_add";