src/Tools/isac/ME/generate.sml
branchisac-update-Isa09-2
changeset 37928 dfec2cf32f77
parent 37926 e6fc98fbcb85
     1.1 --- a/src/Tools/isac/ME/generate.sml	Wed Aug 18 16:03:27 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/generate.sml	Thu Aug 19 12:00:46 2010 +0200
     1.3 @@ -478,7 +478,7 @@
     1.4  	val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
     1.5  	(*val _= writeln("### generate1: is([3],Frm)= "^
     1.6  		       (istate2str (get_istate pt ([3],Frm))));*)
     1.7 -	val f = Sign.string_of_term (sign_of thy) f;
     1.8 +	val f = Syntax.string_of_term (thy2ctxt thy) f;
     1.9      in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.10  
    1.11    | generate1 thy m' _ _ _ =