src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 38757 2b3e054ae6fc
parent 38558 32ad17fe2b9c
child 38759 37a9092de102
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -3033,12 +3033,13 @@
     1.4      "adding alternative introduction rules for code generation of inductive predicates"
     1.5  
     1.6  (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
     1.7 +(* FIXME ... this is important to avoid changing the background theory below *)
     1.8  fun generic_code_pred prep_const options raw_const lthy =
     1.9    let
    1.10      val thy = ProofContext.theory_of lthy
    1.11      val const = prep_const thy raw_const
    1.12      val ctxt = ProofContext.init_global thy
    1.13 -    val lthy' = Local_Theory.theory (PredData.map
    1.14 +    val lthy' = Local_Theory.background_theory (PredData.map
    1.15          (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
    1.16      val thy' = ProofContext.theory_of lthy'
    1.17      val ctxt' = ProofContext.init_global thy'
    1.18 @@ -3063,7 +3064,7 @@
    1.19          val global_thms = ProofContext.export goal_ctxt
    1.20            (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
    1.21        in
    1.22 -        goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
    1.23 +        goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
    1.24            ((case compilation options of
    1.25               Pred => add_equations
    1.26             | DSeq => add_dseq_equations