diff -r 0c4e48deeefe -r 5aef13872723 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Fri Nov 06 13:49:19 2009 +0100
+++ b/src/HOL/FunDef.thy	Fri Nov 06 14:42:42 2009 +0100
@@ -22,7 +22,7 @@
   ("Tools/Function/lexicographic_order.ML")
   ("Tools/Function/pat_completeness.ML")
   ("Tools/Function/fun.ML")
-  ("Tools/Function/induction_scheme.ML")
+  ("Tools/Function/induction_schema.ML")
   ("Tools/Function/termination.ML")
   ("Tools/Function/decompose.ML")
   ("Tools/Function/descent.ML")
@@ -114,13 +114,13 @@
 use "Tools/Function/function.ML"
 use "Tools/Function/pat_completeness.ML"
 use "Tools/Function/fun.ML"
-use "Tools/Function/induction_scheme.ML"
+use "Tools/Function/induction_schema.ML"
 
 setup {* 
   Function.setup
   #> Pat_Completeness.setup
   #> Function_Fun.setup
-  #> Induction_Scheme.setup
+  #> Induction_Schema.setup
 *}
 
 subsection {* Measure Functions *}