diff -r 1500f96707b0 -r 3cfea5bb5e23 thys2/PDerivs.thy
--- a/thys2/PDerivs.thy	Sun Jan 30 23:37:29 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Feb 02 14:52:41 2022 +0000
@@ -12,7 +12,7 @@
   "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"
   by auto
 
-primrec
+fun
   pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
 where
   "pder c ZERO = {}"
@@ -23,7 +23,7 @@
     (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)"
 | "pder c (STAR r) = SEQs (pder c r) (STAR r)"
 
-primrec
+fun
   pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set"
 where
   "pders [] r = {r}"