src/HOL/ex/Predicate_Compile_ex.thy
changeset 32665 8bf46a97ff79
parent 32579 73ad5dbf1034
child 32668 b2de45007537
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -44,7 +44,7 @@
     "partition f [] [] []"
   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-
+ML {* set Toplevel.debug *} 
 code_pred partition .
 
 thm partition.equation