--- a/src/HOL/Transitive_Closure.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Feb 17 13:31:42 2014 +0100
@@ -716,11 +716,11 @@
relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
begin
-primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+old_primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
"relpow 0 R = Id"
| "relpow (Suc n) R = (R ^^ n) O R"
-primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
+old_primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
"relpowp 0 R = HOL.eq"
| "relpowp (Suc n) R = (R ^^ n) OO R"