1.1 --- a/test/Tools/isac/Knowledge/rooteq.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -24,62 +24,62 @@
     1.4  
     1.5  val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
     1.6  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
     1.7 -val result = UnparseC.term2str t_;
     1.8 +val result = UnparseC.term t_;
     1.9  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.10  
    1.11  val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
    1.12  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.13 -val result = UnparseC.term2str t_;
    1.14 +val result = UnparseC.term t_;
    1.15  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.16  
    1.17  val t = (Thm.term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in  x";
    1.18  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.19 -val result = UnparseC.term2str t_;
    1.20 +val result = UnparseC.term t_;
    1.21  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.22  
    1.23  val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in  x";
    1.24  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.25 -val result = UnparseC.term2str t_;
    1.26 +val result = UnparseC.term t_;
    1.27  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.28  
    1.29  val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in  x";
    1.30  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.31 -val result = UnparseC.term2str t_;
    1.32 +val result = UnparseC.term t_;
    1.33  if result <>  "HOL.False"  then error "rooteq.sml: new behaviour:" else ();
    1.34  
    1.35  val t = (Thm.term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
    1.36  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.37 -val result = UnparseC.term2str t_;
    1.38 +val result = UnparseC.term t_;
    1.39  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.40  
    1.41  val t = (Thm.term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
    1.42  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.43 -val result = UnparseC.term2str t_;
    1.44 +val result = UnparseC.term t_;
    1.45  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.46  
    1.47  val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
    1.48  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.49 -val result = UnparseC.term2str t_;
    1.50 +val result = UnparseC.term t_;
    1.51  if result <>  "HOL.False"  then error "rooteq.sml: new behaviour:" else ();
    1.52  
    1.53  val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
    1.54  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.55 -val result = UnparseC.term2str t_;
    1.56 +val result = UnparseC.term t_;
    1.57  if result <>  "HOL.False"  then error "rooteq.sml: new behaviour:" else ();
    1.58  
    1.59  val t = (Thm.term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
    1.60  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.61 -val result = UnparseC.term2str t_;
    1.62 +val result = UnparseC.term t_;
    1.63  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.64  
    1.65  val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in  x";
    1.66  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.67 -val result = UnparseC.term2str t_;
    1.68 +val result = UnparseC.term t_;
    1.69  if result <>  "HOL.False"  then error "rooteq.sml: new behaviour:" else ();
    1.70  
    1.71  val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in  x";
    1.72  val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.73 -val result = UnparseC.term2str t_;
    1.74 +val result = UnparseC.term t_;
    1.75  if result <>  "HOL.True"  then error "rooteq.sml: new behaviour:" else ();
    1.76  
    1.77  
    1.78 @@ -134,7 +134,7 @@
    1.79  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.80  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
    1.81  	 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
    1.82 -if UnparseC.terms2str (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
    1.83 +if UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
    1.84  (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..:
    1.85       [(str2term"25 ~= 0",[])] *)
    1.86  then writeln "should be True\n\
    1.87 @@ -561,7 +561,7 @@
    1.88    ("Test",["sqroot-test","univariate","equation","test"],
    1.89     ["Test","square_equation2"]);
    1.90  val Prog sc = (#scr o get_met) ["Test","square_equation2"];
    1.91 -(writeln o UnparseC.term2str) sc;
    1.92 +(writeln o UnparseC.term) sc;
    1.93  
    1.94  (*val p = e_pos'; val c = []; 
    1.95  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
    1.96 @@ -704,7 +704,7 @@
    1.97    ("Test",["squareroot","univariate","equation","test"],
    1.98     ["Test","square_equation"]);
    1.99   val Prog sc = (#scr o get_met) ["Test","square_equation"];
   1.100 - (writeln o UnparseC.term2str) sc;
   1.101 + (writeln o UnparseC.term) sc;
   1.102  
   1.103  (*val p = e_pos'; val c = []; 
   1.104  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));