--- 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