--- 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)"
--- 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