src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -792,7 +792,7 @@
        induct = induct};
 
     val ctxt3 = ctxt2
-      |> LocalTheory.declaration (fn phi =>
+      |> LocalTheory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, ctxt3) end;