src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -931,7 +931,7 @@
        eqs = eqs'};
 
     val lthy4 = lthy3
-      |> Local_Theory.declaration false (fn phi =>
+      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
         let val result' = transform_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, lthy4) end;