# HG changeset patch
# User bulwahn
# Date 1319006242 -7200
# Node ID df4cbfc5ca4f9d5fa6988a79664dff6beee8c0e2
# Parent  ae8411edd939f2d3cf309dd1a11526f49a6a8214
removing old code generator setup of inductive predicates

diff -r ae8411edd939 -r df4cbfc5ca4f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 19 08:37:21 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 19 08:37:22 2011 +0200
@@ -9,7 +9,6 @@
 imports Typedef Inductive Fun
 uses
   ("Tools/split_rule.ML")
-  ("Tools/inductive_codegen.ML")
   ("Tools/inductive_set.ML")
 begin
 
@@ -1114,9 +1113,6 @@
 
 subsection {* Inductively defined sets *}
 
-use "Tools/inductive_codegen.ML"
-setup Inductive_Codegen.setup
-
 use "Tools/inductive_set.ML"
 setup Inductive_Set.setup