src/HOL/Tools/Datatype/datatype.ML
changeset 32172 c4e55f30d527
parent 32124 954321008785
child 32374 62617ef2c0d0
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 12:33:00 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 18:58:58 2009 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5  fun add_cases_induct infos induction thy =
     1.6    let
     1.7 -    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
     1.8 +    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
     1.9  
    1.10      fun named_rules (name, {index, exhaustion, ...}: info) =
    1.11        [((Binding.empty, nth inducts index), [Induct.induct_type name]),