diff -r 821f038df564 -r 778899c624a6 src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 24 08:51:05 2020 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 24 09:01:48 2020 +0200
@@ -28,7 +28,7 @@
 
   | Derive' of Rule_Set.T      
   | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
-  | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
+  | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
   | End_Detail' of Selem.result
 
   | Empty_Tac_
@@ -41,9 +41,9 @@
   | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
 
   | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
-  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
+  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
   | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
-  | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
+  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
 
   | Specify_Method' of Method.id * Model.ori list * Model.itm list
   | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
@@ -362,7 +362,7 @@
 
   | Derive' of Rule_Set.T
   | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
-  | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
+  | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
   | End_Detail' of Selem.result
 
   | Empty_Tac_
@@ -382,9 +382,9 @@
     Method.id *     (* from new pbt?! filled in specify                                     *)
     Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
   | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
-  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
+  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
   | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
-  | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
+  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
 
   | Specify_Method' of Method.id * Model.ori list * Model.itm list
   | Specify_Problem' of Problem.id *