src/Pure/Isar/spec_rules.ML

 );
 
 val get = Item_Net.content o Rules.get o Context.Proof;
 val get_global = Item_Net.content o Rules.get o Context.Theory;
 
-fun add class (ts, ths) = LocalTheory.declaration
+fun add class (ts, ths) = LocalTheory.declaration true
   (fn phi =>
     let
       val ts' = map (Morphism.term phi) ts;
       val ths' = map (Morphism.thm phi) ths;
     in Rules.map (Item_Net.update (class, (ts', ths'))) end);