--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Aug 26 14:07:11 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Aug 26 14:48:48 2010 +0200
@@ -172,7 +172,7 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = []} *}
values 2 "{y. notB y}"
@@ -187,7 +187,7 @@
inductive equals :: "abc => abc => bool"
where
"equals y' y'"
-ML {* set Code_Prolog.trace *}
+
values 1 "{(y, z). equals y z}"
end