src/HOL/Inductive.thy
changeset 48357 828ace4f75ab
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
--- a/src/HOL/Inductive.thy	Thu Jul 19 12:01:05 2012 +0200
+++ b/src/HOL/Inductive.thy	Thu Jul 19 19:38:39 2012 +0200
@@ -12,7 +12,6 @@
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 uses
-  "Tools/dseq.ML"
   ("Tools/inductive.ML")
   ("Tools/Datatype/datatype_aux.ML")
   ("Tools/Datatype/datatype_prop.ML")