1.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4        val p = lev_dn p;
     1.5  val NONE = (*case*) ini (*of*);
     1.6              val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt;
     1.7 -	          val d = Rule_Set.e_rls (*FIXME: get simplifier from domID*);
     1.8 +	          val d = Rule_Set.empty (*FIXME: get simplifier from domID*);
     1.9       val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
    1.10  Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
    1.11