diff -r 877d6bc38715 -r 7601a1fa20b9 src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Sat May 02 12:13:20 2020 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Sat May 02 15:41:27 2020 +0200
@@ -4,7 +4,7 @@
 
 regular expression for search:
 
-Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
+Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
 
 *)
 signature TACTIC =
@@ -21,7 +21,6 @@
   | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
   | Specify_Theory' of ThyC.id
   (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
-  | CAScmd' of term
   | Calculate' of ThyC.id * string * term * (term * ThmC.T)
   | Check_Postcond' of Problem.id * term
   | Check_elementwise' of term * TermC.as_string * Selem.result
@@ -55,7 +54,6 @@
   | Specify_Problem of Problem.id
   | Specify_Theory of ThyC.id
   (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
-  | CAScmd of TermC.as_string
   | Calculate of string
   | Check_Postcond of Problem.id
   | Check_elementwise of TermC.as_string
@@ -121,7 +119,6 @@
   | Specify_Problem of Problem.id
   | Specify_Theory of ThyC.id
   (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
-  | CAScmd of TermC.as_string
   | Calculate of string
   | Check_Postcond of Problem.id
   | Check_elementwise of TermC.as_string
@@ -172,7 +169,6 @@
 
   | Take cterm'             => "Take " ^ quote cterm'
   | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
-  | CAScmd cterm'           => "CAScmd " ^ quote cterm'
 
   | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
   | Or_to_List              => "Or_to_List "
@@ -210,7 +206,6 @@
 
   | Take _ => "Take"
   | Subproblem _ => "Subproblem"
-  | CAScmd _ => "CAScmd"
 
   | Check_elementwise _ => "Check_elementwise"
   | Or_to_List => "Or_to_List "
@@ -324,7 +319,6 @@
           (bool * term) list)) (* individual preconditions marked true/false *)
   | Specify_Theory' of ThyC.id
   (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
-  | CAScmd' of term
   | Calculate' of ThyC.id * string * term * (term * ThmC.T)
   | Check_Postcond' of   (* last step in solving a (sub-)Problem             *)
       Problem.id *       (* id of the Problem to be checked                  *)
@@ -399,7 +393,6 @@
   | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)
   | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 
     "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
-  | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
 
   | Empty_Tac_ => "Empty_Tac_"
   | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"