1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -34,13 +34,13 @@
     1.4      | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
     1.5  
     1.6  val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst 
     1.7 -  (num_str @{thm "int_isolate_add"}) t; term2str t;
     1.8 +  (num_str @{thm "int_isolate_add"}) t; UnparseC.term2str t;
     1.9  
    1.10  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
    1.11 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.12 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term2str t;
    1.13  
    1.14  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
    1.15 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.16 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term2str t;
    1.17  
    1.18  "----------- mathengine with usecase1 -------------------";
    1.19  "----------- mathengine with usecase1 -------------------";
    1.20 @@ -72,10 +72,10 @@
    1.21      | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
    1.22  
    1.23  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
    1.24 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.25 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term2str t;
    1.26  
    1.27  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
    1.28 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.29 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term2str t;
    1.30  
    1.31  
    1.32  "----------- mathengine with usecase2 -------------------";