src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -192,7 +192,7 @@
        proc = proc,
        identifier = identifier};
   in
-    lthy |> Local_Theory.declaration false (fn phi => fn context =>
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;