diff -r 183e35109dda -r dfec2cf32f77 src/Tools/isac/ME/generate.sml
--- a/src/Tools/isac/ME/generate.sml	Wed Aug 18 16:03:27 2010 +0200
+++ b/src/Tools/isac/ME/generate.sml	Thu Aug 19 12:00:46 2010 +0200
@@ -478,7 +478,7 @@
 	val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
 	(*val _= writeln("### generate1: is([3],Frm)= "^
 		       (istate2str (get_istate pt ([3],Frm))));*)
-	val f = Sign.string_of_term (sign_of thy) f;
+	val f = Syntax.string_of_term (thy2ctxt thy) f;
     in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
 
   | generate1 thy m' _ _ _ =