# HG changeset patch
# User haftmann
# Date 1236783409 -3600
# Node ID 955190fa639b23a80e027ba22c793dae14275154
# Parent  e3641cac56fa693d28595e3be8495c254d939bb4
stripped dead code

diff -r e3641cac56fa -r 955190fa639b src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Mar 11 15:56:49 2009 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Mar 11 15:56:49 2009 +0100
@@ -264,7 +264,6 @@
 
 structure Lib =
 struct
-fun wrap b e s = String.concat[b,s,e]
 
 fun assoc x =
     let
@@ -280,9 +279,6 @@
           | itr (a::rst) = i=a orelse itr rst
     in itr L end;
 
-fun mk_set [] = []
-  | mk_set (a::rst) = insert (op =) a (mk_set rst)
-
 fun [] union S = S
   | S union [] = S
   | (a::rst) union S2 = rst union (insert (op =) a S2)