# HG changeset patch
# User wenzelm
# Date 1165363977 -3600
# Node ID 38f6cb45ce2453475dd15e719ccfba251954bef7
# Parent  8a6bf9d7c7511c021c24c86585adc249d91e419c
simplified ML bindings;

diff -r 8a6bf9d7c751 -r 38f6cb45ce24 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Wed Dec 06 01:12:56 2006 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Wed Dec 06 01:12:57 2006 +0100
@@ -31,11 +31,6 @@
 structure TypecopyPackage: TYPECOPY_PACKAGE =
 struct
 
-(* theory context reference *)
-
-val univ_witness = thm "Set.UNIV_witness"
-
-
 (* theory data *)
 
 type info = {