--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Mar 03 18:32:01 2009 +0100
@@ -453,7 +453,7 @@
Proof.theorem_i NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Sign.base_name names);
- val rec_qualified = Binding.qualify rec_name;
+ val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
(intrs ~~ induct_cases);