# HG changeset patch
# User wenzelm
# Date 1243784753 -7200
# Node ID 72eeb1b4e006c42bd049b7e549497f5fea11dd56
# Parent  6974449ddea96eb46548a14a262beafb49af542d
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;

diff -r 6974449ddea9 -r 72eeb1b4e006 src/HOL/ex/predicate_compile.ML
--- 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);