# HG changeset patch
# User haftmann
# Date 1254295518 -7200
# Node ID d498770eefdcb4d14103fc0bffc99a15a8d67906
# Parent  995b9c763c66fb02fed08787006a41fa106cb162# Parent  461afcc6acb8c5a5e022cf054a56869f3f2074ce
merged

diff -r 995b9c763c66 -r d498770eefdc NEWS
--- a/NEWS	Wed Sep 30 00:57:28 2009 +0200
+++ b/NEWS	Wed Sep 30 09:25:18 2009 +0200
@@ -18,6 +18,10 @@
 
 *** HOL ***
 
+* Most rules produced by inductive and datatype package
+have mandatory prefixes.
+INCOMPATIBILITY.
+
 * New proof method "smt" for a combination of first-order logic
 with equality, linear and nonlinear (natural/integer/real)
 arithmetic, and fixed-size bitvectors; there is also basic
diff -r 995b9c763c66 -r d498770eefdc src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Sep 30 00:57:28 2009 +0200
+++ b/src/HOL/Nat.thy	Wed Sep 30 09:25:18 2009 +0200
@@ -86,7 +86,7 @@
   assumes "P 0"
     and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   shows "P n"
-  using assms by (rule nat.induct) 
+  using assms by (rule nat.induct)
 
 declare nat.exhaust [case_names 0 Suc, cases type: nat]
 
diff -r 995b9c763c66 -r d498770eefdc src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 30 00:57:28 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Sep 30 09:25:18 2009 +0200
@@ -683,7 +683,7 @@
       elims raw_induct ctxt =
   let
     val rec_name = Binding.name_of rec_binding;
-    val rec_qualified = Binding.qualify false rec_name;
+    fun rec_qualified qualified = Binding.qualify qualified rec_name;
     val intr_names = map Binding.name_of intr_bindings;
     val ind_case_names = RuleCases.case_names intr_names;
     val induct =
@@ -698,29 +698,29 @@
     val (intrs', ctxt1) =
       ctxt |>
       LocalTheory.notes kind
-        (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
+        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
            [Attrib.internal (K (ContextRules.intro_query NONE)),
             Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
-      LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
+      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note kind ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "cases"),
+        LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
           [Attrib.internal (K (RuleCases.case_names cases)),
            Attrib.internal (K (RuleCases.consumes 1)),
            Attrib.internal (K (Induct.cases_pred name)),
            Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
       LocalTheory.note kind
-        ((rec_qualified (Binding.name (coind_prefix coind ^ "induct")),
+        ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
     val ctxt3 = if no_ind orelse coind then ctxt2 else
       let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
       in
         ctxt2 |>
-        LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
+        LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
           inducts |> map (fn (name, th) => ([th],
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1)),