diff -r 0042fe0bc764 -r 82428ca0d23e test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 13:27:55 2020 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 15:31:23 2020 +0200
@@ -244,7 +244,7 @@
 				      eval_occur_exactly_in 
 					  "#eval_occur_exactly_in_"))
 			       ]) 
-		  false bdvs (num_str @{separate_bdvs_add) t;
+		  false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
 (writeln o UnparseC.term) t;
 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
 then () else error "rewrite.sml rewrite_inst_ bdvs";
@@ -502,7 +502,7 @@
 "----------- 2011 thms with axclasses -------------------";
 "----------- 2011 thms with axclasses -------------------";
 "----------- 2011 thms with axclasses -------------------";
-val thm = num_str @{thm div_by_1};
+val thm = ThmC.numerals_to_Free @{thm div_by_1};
 val prop = Thm.prop_of thm;
 atomty prop;                                     (*Type 'a*)
 val t = str2term "(2*x)/1";                      (*Type real*)
@@ -741,7 +741,7 @@
   NONE => ()
 | _ => writeln "parse does NOT take patterns with '?'";
 
-val t1 = (#prop o Thm.rep_thm) (num_str thm);
+val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
 if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
 
 val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
@@ -754,7 +754,7 @@
 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
   ..gives another strange thm; but it is used and works with rewriting: *);
 
-val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
+val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
 
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -773,7 +773,7 @@
   NONE => ()
 | _ => writeln "parse does NOT take patterns with '?'";
 
-val t1 = (#prop o Thm.rep_thm) (num_str thm);
+val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
 if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
 
 val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
@@ -786,7 +786,7 @@
 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
   gives another strange thm; but it is used and words with rewriting: *);
 
-val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
+val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
 
 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";