src/HOL/Tools/inductive_package.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30435 e62d6ecab6ad
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -698,7 +698,7 @@
     1.4        ctxt1 |>
     1.5        LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
     1.6        fold_map (fn (name, (elim, cases)) =>
     1.7 -        LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
     1.8 +        LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"),
     1.9            [Attrib.internal (K (RuleCases.case_names cases)),
    1.10             Attrib.internal (K (RuleCases.consumes 1)),
    1.11             Attrib.internal (K (Induct.cases_pred name)),