Use LocalTheory.full_name instead of Sign.full_name, because the latter does
not work properly for locales.

--- a/src/HOL/Tools/inductive_package.ML	Wed Feb 25 11:07:10 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Feb 25 11:20:34 2009 +0100
@@ -738,7 +738,7 @@
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (LocalTheory.full_name ctxt o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule ctxt cs params) intros));
 

--- a/src/HOL/Tools/inductive_set_package.ML	Wed Feb 25 11:07:10 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Feb 25 11:20:34 2009 +0100
@@ -503,7 +503,7 @@
       if Binding.is_empty alt_name then
         Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
       else alt_name;
-    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
     val (intrs', elims', induct, ctxt4) =