src/HOL/Tools/typecopy_package.ML
changeset 21675 38f6cb45ce24
parent 20855 9f60d493c8fe
child 21708 45e7491bea47
--- 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 = {