src/HOL/Tools/inductive_package.ML
changeset 30435 e62d6ecab6ad
parent 30364 577edc39b501
child 30486 9cdc7ce0e389
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 11 15:38:25 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 11 15:42:19 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 (Long_Name.qualify (Long_Name.base_name name) "cases"),
     1.8 +        LocalTheory.note kind ((Binding.qualified_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)),