provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
--- a/src/HOL/ex/predicate_compile.ML Sun May 31 16:41:52 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Sun May 31 17:45:53 2009 +0200
@@ -31,6 +31,8 @@
(* debug stuff *)
+fun makestring _ = "?"; (* FIXME dummy *)
+
fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);