# HG changeset patch
# User wenzelm
# Date 1164207495 -3600
# Node ID 2d3f477118c20d5447abbf258aa1fd04ed043989
# Parent  abaf43b011ee7f98f60e2900a85f4ff21b18a484
more careful declaration of "intros" as Pure.intro;

diff -r abaf43b011ee -r 2d3f477118c2 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Nov 22 12:01:59 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 22 15:58:15 2006 +0100
@@ -663,12 +663,12 @@
       note_theorems
         (map (NameSpace.qualified rec_name) intr_names ~~
          intr_atts ~~
-         map (fn th => [([th], [])]) (ProofContext.export ctxt1 ctxt intrs)) |>>
+         map (fn th => [([th], [Attrib.internal (ContextRules.intro_query NONE)])])
+           (ProofContext.export ctxt1 ctxt intrs)) |>>
       map (hd o snd); (* FIXME? *)
     val (((_, elims'), (_, [induct'])), ctxt3) =
       ctxt2 |>
-      note_theorem ((NameSpace.qualified rec_name "intros",
-          [Attrib.internal (ContextRules.intro_query NONE)]), intrs') ||>>
+      note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
         note_theorem ((NameSpace.qualified (Sign.base_name name) "cases",
           [Attrib.internal (RuleCases.case_names cases),