diff -r 7fb011dd51de -r 8c20eb9a388d src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:57 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:58 2010 +0200
@@ -12,14 +12,6 @@
 
 code_pred append .
 
-ML {*
-  tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}]))
-*}
-
-ML {*
-  Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
-*}
-
-values "{(x, y, z). append x y z}"
+values 3 "{((x::'b list), y, z). append x y z}"
 
 end