src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:55 2010 +0200
@@ -182,4 +182,12 @@
 
 values 5 "{y. notAB y}"
 
+section {* Example prolog conform variable names *}
+
+inductive equals :: "abc => abc => bool"
+where
+  "equals y' y'"
+ML {* set Code_Prolog.trace *}
+values 1 "{(y, z). equals y z}"
+
 end