src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -192,7 +192,7 @@
        identifier = identifier}
       |> morph_simproc (LocalTheory.target_morphism lthy);
   in
-    lthy |> LocalTheory.declaration (fn phi =>
+    lthy |> LocalTheory.declaration false (fn phi =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;