src/Tools/isac/Interpret/generate.sml
branchdecompose-isar
changeset 41984 3f614796186e
parent 41983 4c49adbfadab
child 41990 99e83a0bea44
     1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed May 11 16:51:30 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu May 12 08:26:02 2011 +0200
     1.3 @@ -479,7 +479,7 @@
     1.4        let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
     1.5  	      val (pt,c) =
     1.6            cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
     1.7 -        val pt = update_ctxt pt (p, Res) ctxt (*FIXME.WN110511*)   
     1.8 +        val pt = update_pbl_ctxt pt p ctxt (*FIXME.WN110511*)   
     1.9  	      val f = Syntax.string_of_term (thy2ctxt thy) f;
    1.10        in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.11