simplified ML bindings;
authorwenzelm
Wed, 06 Dec 2006 01:12:57 +0100
changeset 21675 38f6cb45ce24
parent 21674 8a6bf9d7c751
child 21676 a45af03f6827
simplified ML bindings;
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 = {