--- a/thys2/PDerivs.thy	Mon Feb 21 23:38:26 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Mar 02 11:43:41 2022 +0000
@@ -400,8 +400,9 @@
    apply(rule subset_trans)
   thm pders_STAR
      apply(rule pders_STAR)
-     apply(simp)
-    apply(auto simp add: pders_Set_def)[1]
+    apply(simp)
+   apply(auto simp add: pders_Set_def)[1]
+(* rest of SEQ case *)  
   apply(simp)
   apply(rule conjI)
    apply blast