provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
authorwenzelm
Sun, 31 May 2009 17:45:53 +0200
changeset 31320 72eeb1b4e006
parent 31319 6974449ddea9
child 31321 fe786d4633b9
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
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);