diff -r 64d1b02327a4 -r 5cab031e2344 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Sat Oct 16 20:21:13 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sat Oct 16 20:32:25 2021 +0200
@@ -1692,14 +1692,6 @@
 
 val list_mk_type = Utils.end_itlist (curry (op -->));
 
-fun front_last [] = raise TFL_ERR "front_last" "empty list"
-  | front_last [x] = ([],x)
-  | front_last (h::t) =
-     let val (pref,x) = front_last t
-     in
-        (h::pref,x)
-     end;
-
 
 (*---------------------------------------------------------------------------
  * The next function is common to pattern-match translation and
@@ -2057,8 +2049,6 @@
 end;
 
 
-fun givens pats = map pat_of (filter given pats);
-
 fun post_definition ctxt meta_tflCongs (def, pats) =
  let val thy = Proof_Context.theory_of ctxt
      val tych = Thry.typecheck thy