diff --git a/library/theories/String.scala b/library/theories/String.scala
index 8057c2d2a72700349574a95e56293ee6a2e9620d..541e90261057ac0fe321c14dfda3e2d276a108ea 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -30,11 +30,13 @@ sealed abstract class String {
     case _ => this
   }
   
+  @isabelle.noBody()
   def takeI(i: Int): String = this match {
     case StringCons(head, tail) if i > 0 => StringCons(head, tail takeI (i - 1))
     case _ => StringNil()
   }
 
+  @isabelle.noBody()
   def dropI(i: Int): String = this match {
     case StringCons(head, tail) if i > 0 => tail dropI (i - 1)
     case _ => this