diff -r 23c143ffb22f -r 148d369e6b71 src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 20 11:11:56 2020 +0100
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 20 11:48:59 2020 +0100
@@ -102,9 +102,10 @@
   | Tac of string
   | Take of Rule.cterm' | Take_Inst of Rule.cterm'
   val tac2str : input -> string
+  val is_empty_tac : input -> bool
 
+(*//-------------------------------------------------------------- only AFTER ctree.sml required *)
   val eq_tac : input * input -> bool
-  val is_empty_tac : input -> bool
   val is_rewtac : input -> bool
   val is_rewset : input -> bool
   val rls_of : input -> Rule.rls'