diff -r d07959fabde6 -r 2b3e054ae6fc src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -3033,12 +3033,13 @@
     "adding alternative introduction rules for code generation of inductive predicates"
 
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
+(* FIXME ... this is important to avoid changing the background theory below *)
 fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
     val ctxt = ProofContext.init_global thy
-    val lthy' = Local_Theory.theory (PredData.map
+    val lthy' = Local_Theory.background_theory (PredData.map
         (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
     val thy' = ProofContext.theory_of lthy'
     val ctxt' = ProofContext.init_global thy'
@@ -3063,7 +3064,7 @@
         val global_thms = ProofContext.export goal_ctxt
           (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       in
-        goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
+        goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
           ((case compilation options of
              Pred => add_equations
            | DSeq => add_dseq_equations