src/HOL/Tools/record.ML
changeset 32748 887c68b70f7d
parent 32745 192d58483fdf
child 32749 3282c12a856c
--- a/src/HOL/Tools/record.ML	Fri Sep 11 15:57:16 2009 +1000
+++ b/src/HOL/Tools/record.ML	Fri Sep 11 18:03:30 2009 +1000
@@ -1721,8 +1721,7 @@
            [("ext_inject", inject),
             ("ext_induct", induct),
             ("ext_surjective", surject),
-            ("ext_split", split_meta),
-            ("ext_def", ext_def)]
+            ("ext_split", split_meta)]
 
   in (thm_thy,extT,induct',inject',split_meta',ext_def')
   end;