# HG changeset patch
# User wenzelm
# Date 902761562 -7200
# Node ID b755c7240348914ed845e0fa7a7381e73c5a3984
# Parent  41b949f3b8acbbabe3eb019e85495e22438516d9
suffix, unsuffix moved to Pure/library.ML;

diff -r 41b949f3b8ac -r b755c7240348 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Aug 10 17:04:28 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Aug 10 17:06:02 1998 +0200
@@ -37,21 +37,6 @@
 
 (*** utilities ***)
 
-(* string suffixes *)
-
-fun suffix sfx s = s ^ sfx;
-
-fun unsuffix sfx s =
-  let
-    val cs = explode s;
-    val prfx_len = size s - size sfx;
-  in
-    if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
-      implode (take (prfx_len, cs))
-    else raise LIST "unsuffix"
-  end;
-
-
 (* definitions and equations *)
 
 infix 0 :== === ;