# HG changeset patch
# User wenzelm
# Date 1248431580 -7200
# Node ID 220abde9962b59d833be2f461d9882f9f60f3d34
# Parent  541b357299923fc7a46fd1f776b2665351df56e0
renamed functor InductFun to Induct;

diff -r 541b35729992 -r 220abde9962b src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/FOL/FOL.thy	Fri Jul 24 12:33:00 2009 +0200
@@ -360,7 +360,7 @@
 text {* Method setup. *}
 
 ML {*
-  structure Induct = InductFun
+  structure Induct = Induct
   (
     val cases_default = @{thm case_split}
     val atomize = @{thms induct_atomize}
diff -r 541b35729992 -r 220abde9962b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
@@ -1446,7 +1446,7 @@
 text {* Method setup. *}
 
 ML {*
-structure Induct = InductFun
+structure Induct = Induct
 (
   val cases_default = @{thm case_split}
   val atomize = @{thms induct_atomize}
diff -r 541b35729992 -r 220abde9962b src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/Tools/induct.ML	Fri Jul 24 12:33:00 2009 +0200
@@ -70,7 +70,7 @@
   val setup: theory -> theory
 end;
 
-functor InductFun(Data: INDUCT_DATA): INDUCT =
+functor Induct(Data: INDUCT_DATA): INDUCT =
 struct