src/Tools/isac/Interpret/generate.sml
branchdecompose-isar
changeset 41990 99e83a0bea44
parent 41984 3f614796186e
child 41993 2301fe2b9f9c
     1.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri May 13 14:15:59 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 13 17:19:38 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_pbl_ctxt pt p ctxt (*FIXME.WN110511*)   
     1.8 +        val pt = update_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