diff -r 3d3ebc0c927c -r 329f1b4d9d16 src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Thu Sep 20 12:09:09 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Thu Sep 20 12:10:23 2007 +0200
@@ -330,8 +330,8 @@
 		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
 		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
 		val right = (indexed "C" c)^" "^(string_of_tuple xs)
-		val debug_lazy = "(print x"^(string_of_int (strict_args - 1))^";"
-		val right = if strict_args < the (arity_of c) then debug_lazy^"raise AM_SML.Run \"unresolved lazy call: "^(string_of_int c)^"\")" else right		
+		val message = "(\"unresolved lazy call: "^(string_of_int c)^", \"^(makestring x"^(string_of_int (strict_args - 1))^"))"		
+		val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right		
 	    in
 		(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right
 	    end
@@ -363,7 +363,7 @@
 	    end
         
 	fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else ""
-	val _ = writelist [        
+	val _ = writelist [                   
 		"structure "^name^" = struct",
 		"",
 		"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
@@ -456,7 +456,7 @@
 		"",
 		"fun export term = AM_SML.save_result (\""^code^"\", convert term)",
 		"",
-                "val _ = AM_SML.set_compiled_rewriter (fn t => convert (eval [] t))",
+                "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))",
                 "",
 		"end"]
     in