diff -r 6a27e86cc2e7 -r 9e712280cc37 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -40,8 +40,8 @@
     val (fname, ftype) = dest_Const recfun handle TERM _ =>
       raise RecError "function is not declared as constant in theory";
 
-    val (ls_frees, rest)  = take_prefix is_Free args;
-    val (middle, rs_frees) = take_suffix is_Free rest;
+    val (ls_frees, rest)  = chop_prefix is_Free args;
+    val (middle, rs_frees) = chop_suffix is_Free rest;
 
     val (constr, cargs_frees) =
       if null middle then raise RecError "constructor missing"