# HG changeset patch
# User berghofe
# Date 1235557234 -3600
# Node ID f631fb528277cfc6d742812de22652e47471daec
# Parent  fe6eac03b81635843060032f24af7f0a03231fd8
Use LocalTheory.full_name instead of Sign.full_name, because the latter does
not work properly for locales.

diff -r fe6eac03b816 -r f631fb528277 src/HOL/Tools/inductive_package.ML
--- 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));
 
diff -r fe6eac03b816 -r f631fb528277 src/HOL/Tools/inductive_set_package.ML
--- 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) =