--- a/src/HOL/Tools/inductive_package.ML Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sun Mar 08 17:26:14 2009 +0100
@@ -698,7 +698,7 @@
ctxt1 |>
LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
- LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
+ LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"),
[Attrib.internal (K (RuleCases.case_names cases)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),