--- 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