src/Pure/Isar/spec_rules.ML

--- a/src/Pure/Isar/spec_rules.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -50,7 +50,7 @@
   let
     val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
   in
-    lthy |> Local_Theory.declaration true
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi =>
         let
           val (ts', ths') =