# HG changeset patch
# User wenzelm
# Date 1190827075 -7200
# Node ID 4d2f2e375fa1af9c1079c26f19a8c6183a875c35
# Parent  21d1cdab2d8cee2300232ce5d95d73ca1acb598f
removed dead code;

diff -r 21d1cdab2d8c -r 4d2f2e375fa1 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Sep 26 11:27:46 2007 +0200
+++ b/src/HOL/Inductive.thy	Wed Sep 26 19:17:55 2007 +0200
@@ -9,8 +9,6 @@
 imports FixedPoint Sum_Type
 uses
   ("Tools/inductive_package.ML")
-  (*("Tools/inductive_set_package.ML")
-  ("Tools/inductive_realizer.ML")*)
   "Tools/dseq.ML"
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")