1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4  				      eval_occur_exactly_in 
     1.5  					  "#eval_occur_exactly_in_"))
     1.6  			       ]) 
     1.7 -		  false bdvs (num_str @{separate_bdvs_add) t;
     1.8 +		  false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
     1.9  (writeln o UnparseC.term) t;
    1.10  if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
    1.11  then () else error "rewrite.sml rewrite_inst_ bdvs";
    1.12 @@ -502,7 +502,7 @@
    1.13  "----------- 2011 thms with axclasses -------------------";
    1.14  "----------- 2011 thms with axclasses -------------------";
    1.15  "----------- 2011 thms with axclasses -------------------";
    1.16 -val thm = num_str @{thm div_by_1};
    1.17 +val thm = ThmC.numerals_to_Free @{thm div_by_1};
    1.18  val prop = Thm.prop_of thm;
    1.19  atomty prop;                                     (*Type 'a*)
    1.20  val t = str2term "(2*x)/1";                      (*Type real*)
    1.21 @@ -741,7 +741,7 @@
    1.22    NONE => ()
    1.23  | _ => writeln "parse does NOT take patterns with '?'";
    1.24  
    1.25 -val t1 = (#prop o Thm.rep_thm) (num_str thm);
    1.26 +val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
    1.27  if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
    1.28  
    1.29  val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
    1.30 @@ -754,7 +754,7 @@
    1.31  val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
    1.32    ..gives another strange thm; but it is used and works with rewriting: *);
    1.33  
    1.34 -val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.35 +val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
    1.36  if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
    1.37  
    1.38  (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.39 @@ -773,7 +773,7 @@
    1.40    NONE => ()
    1.41  | _ => writeln "parse does NOT take patterns with '?'";
    1.42  
    1.43 -val t1 = (#prop o Thm.rep_thm) (num_str thm);
    1.44 +val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
    1.45  if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
    1.46  
    1.47  val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
    1.48 @@ -786,7 +786,7 @@
    1.49  val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
    1.50    gives another strange thm; but it is used and words with rewriting: *);
    1.51  
    1.52 -val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.53 +val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
    1.54  if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
    1.55  
    1.56  "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";