diff -r 07a042166900 -r e7910a62eaf2 src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 22 11:06:48 2020 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 22 11:23:30 2020 +0200
@@ -199,7 +199,7 @@
 
 fun input_to_string ma = case ma of
     Init_Proof (ppc, spec)  => 
-      "Init_Proof "^(pair2str (strs2str ppc, Spec.spec2str spec))
+      "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
   | Model_Problem           => "Model_Problem "
   | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 
   | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 
@@ -409,7 +409,7 @@
   | Take' of term
 
 fun string_of ma = case ma of
-    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.spec2str spec)
+    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
   | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
   | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
     strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"