renamed functor InductFun to Induct;
authorwenzelm
Fri Jul 24 12:33:00 2009 +0200 (2009-07-24)
changeset 32171220abde9962b
parent 32170 541b35729992
child 32172 c4e55f30d527
renamed functor InductFun to Induct;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/Tools/induct.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Jul 24 12:32:43 2009 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Jul 24 12:33:00 2009 +0200
     1.3 @@ -360,7 +360,7 @@
     1.4  text {* Method setup. *}
     1.5  
     1.6  ML {*
     1.7 -  structure Induct = InductFun
     1.8 +  structure Induct = Induct
     1.9    (
    1.10      val cases_default = @{thm case_split}
    1.11      val atomize = @{thms induct_atomize}
     2.1 --- a/src/HOL/HOL.thy	Fri Jul 24 12:32:43 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
     2.3 @@ -1446,7 +1446,7 @@
     2.4  text {* Method setup. *}
     2.5  
     2.6  ML {*
     2.7 -structure Induct = InductFun
     2.8 +structure Induct = Induct
     2.9  (
    2.10    val cases_default = @{thm case_split}
    2.11    val atomize = @{thms induct_atomize}
     3.1 --- a/src/Tools/induct.ML	Fri Jul 24 12:32:43 2009 +0200
     3.2 +++ b/src/Tools/induct.ML	Fri Jul 24 12:33:00 2009 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4    val setup: theory -> theory
     3.5  end;
     3.6  
     3.7 -functor InductFun(Data: INDUCT_DATA): INDUCT =
     3.8 +functor Induct(Data: INDUCT_DATA): INDUCT =
     3.9  struct
    3.10  
    3.11