# HG changeset patch
# User bulwahn
# Date 1246370292 -7200
# Node ID 39bff8d9b032c861818cd3606739d910ce349ec4
# Parent  4e03a2cdf61163378de8cdc71e028b74d3847f84
commented trancl example; added debug message

diff -r 4e03a2cdf611 -r 39bff8d9b032 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 30 14:55:06 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 30 15:58:12 2009 +0200
@@ -62,7 +62,7 @@
 by auto
 
 (* Setup requires quick and dirty proof *)
-
+(*
 code_pred tranclp
 proof -
   case tranclp
@@ -70,7 +70,7 @@
 qed
 
 thm tranclp.equation
-
+*)
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
diff -r 4e03a2cdf611 -r 39bff8d9b032 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Jun 30 14:55:06 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 30 15:58:12 2009 +0200
@@ -1404,7 +1404,7 @@
   val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
   val pred_mode =
     maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses' 
-  val _ = tracing "Proving equations..."
+  val _ = Output.tracing "Proving equations..."
   val result_thms =
     prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
   val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss