test/Tools/isac/MathEngBasic/rewrite.sml
changeset 60337 cbad4e18e91b
parent 60336 dcb37736d573
child 60339 0d22a6bf1fc6
     1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -474,7 +474,7 @@
     1.4  "----------- 2011 thms with axclasses ----------------------------------------------------------";
     1.5  "----------- 2011 thms with axclasses ----------------------------------------------------------";
     1.6  "----------- 2011 thms with axclasses ----------------------------------------------------------";
     1.7 -val thm = ThmC.numerals_to_Free @{thm div_by_1};
     1.8 +val thm = @{thm div_by_1};
     1.9  val prop = Thm.prop_of thm;
    1.10  TermC.atomty prop;                                     (*Type 'a*)
    1.11  val t = TermC.str2term "(2*x)/1";                      (*Type real*)