# HG changeset patch
# User bulwahn
# Date 1282826928 -7200
# Node ID 4a4be1be0faebcf31591b4a05ff2cc11dc0c6c51
# Parent  499135eb21ec5698a343a3c55ca1d90105f35834
adapted examples; tuned

diff -r 499135eb21ec -r 4a4be1be0fae src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- 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