1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Tue Aug 10 10:27:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Tue Aug 10 11:01:18 2021 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4        let
     1.5    	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
     1.6    	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
     1.7 -  	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
     1.8 +  	    val f = Syntax.string_of_term ctxt f
     1.9        in
    1.10          ((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
    1.11        end