1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Tue Mar 31 14:05:10 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Mar 31 15:43:33 2020 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    datatype input = datatype Tactic_Def.input
     1.5    val tac2str : input -> string
     1.6    val tac2IDstr : input -> string
     1.7 -  val is_empty_tac : input -> bool
     1.8 +  val is_empty : input -> bool
     1.9  
    1.10  (*//-------------------------------------------------------------- only AFTER ctree.sml required *)
    1.11    val eq_tac : input * input -> bool
    1.12 @@ -49,7 +49,7 @@
    1.13  
    1.14  val tac2str = Tactic_Def.tac2str
    1.15  val tac2IDstr = Tactic_Def.tac2IDstr
    1.16 -val is_empty_tac = Tactic_Def.is_empty_tac
    1.17 +val is_empty = Tactic_Def.is_empty
    1.18  
    1.19  fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
    1.20    | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2