1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -176,9 +176,9 @@
     1.4       val t = Const (const, T)
     1.5       val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
     1.6    in
     1.7 -    if (is_inductify options) then
     1.8 +    if is_inductify options then
     1.9        let
    1.10 -        val lthy' = Local_Theory.theory (preprocess options t) lthy
    1.11 +        val lthy' = Local_Theory.background_theory (preprocess options t) lthy
    1.12          val const =
    1.13            case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
    1.14              SOME c => c

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 13:09:12 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 15:48:08 2010 +0200
     2.3 @@ -3033,12 +3033,13 @@
     2.4      "adding alternative introduction rules for code generation of inductive predicates"
     2.5  
     2.6  (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
     2.7 +(* FIXME ... this is important to avoid changing the background theory below *)
     2.8  fun generic_code_pred prep_const options raw_const lthy =
     2.9    let
    2.10      val thy = ProofContext.theory_of lthy
    2.11      val const = prep_const thy raw_const
    2.12      val ctxt = ProofContext.init_global thy
    2.13 -    val lthy' = Local_Theory.theory (PredData.map
    2.14 +    val lthy' = Local_Theory.background_theory (PredData.map
    2.15          (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
    2.16      val thy' = ProofContext.theory_of lthy'
    2.17      val ctxt' = ProofContext.init_global thy'
    2.18 @@ -3063,7 +3064,7 @@
    2.19          val global_thms = ProofContext.export goal_ctxt
    2.20            (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
    2.21        in
    2.22 -        goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
    2.23 +        goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
    2.24            ((case compilation options of
    2.25               Pred => add_equations
    2.26             | DSeq => add_dseq_equations

     3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 13:09:12 2010 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 15:48:08 2010 +0200
     3.3 @@ -77,7 +77,8 @@
     3.4    Typedef.add_typedef false NONE (qty_name, vs, mx) 
     3.5      (typedef_term rel rty lthy) NONE typedef_tac lthy
     3.6  *)
     3.7 -   Local_Theory.theory_result
     3.8 +(* FIXME should really use local typedef here *)
     3.9 +   Local_Theory.background_theory_result
    3.10       (Typedef.add_typedef_global false NONE
    3.11         (qty_name, map (rpair dummyS) vs, mx)
    3.12           (typedef_term rel rty lthy)

     4.1 --- a/src/HOL/Tools/typedef.ML	Thu Aug 26 13:09:12 2010 +0200
     4.2 +++ b/src/HOL/Tools/typedef.ML	Thu Aug 26 15:48:08 2010 +0200
     4.3 @@ -186,7 +186,8 @@
     4.4            ||> Thm.term_of;
     4.5  
     4.6          val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
     4.7 -          Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
     4.8 +          Local_Theory.background_theory_result
     4.9 +            (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
    4.10  
    4.11          val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
    4.12          val typedef =
    4.13 @@ -246,7 +247,7 @@
    4.14        in
    4.15          lthy2
    4.16          |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
    4.17 -        |> Local_Theory.theory (Typedef_Interpretation.data full_tname)
    4.18 +        |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
    4.19          |> pair (full_tname, info)
    4.20        end;
    4.21  

     5.1 --- a/src/Pure/Isar/class.ML	Thu Aug 26 13:09:12 2010 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 26 15:48:08 2010 +0200
     5.3 @@ -482,7 +482,7 @@
     5.4  
     5.5  val type_name = sanitize_name o Long_Name.base_name;
     5.6  
     5.7 -fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
     5.8 +fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
     5.9      (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
    5.10    ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
    5.11    ##> Local_Theory.target synchronize_inst_syntax;
    5.12 @@ -572,7 +572,7 @@
    5.13      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    5.14      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    5.15      fun after_qed' results =
    5.16 -      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
    5.17 +      Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
    5.18        #> after_qed;
    5.19    in
    5.20      lthy

     6.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
     6.2 +++ b/src/Pure/Isar/expression.ML	Thu Aug 26 15:48:08 2010 +0200
     6.3 @@ -824,8 +824,9 @@
     6.4      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     6.5      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
     6.6  
     6.7 -    fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
     6.8 -      (note_eqns_register deps witss attrss eqns export export');
     6.9 +    fun after_qed witss eqns =
    6.10 +      (ProofContext.background_theory o Context.theory_map)
    6.11 +        (note_eqns_register deps witss attrss eqns export export');
    6.12  
    6.13    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    6.14  

     7.1 --- a/src/Pure/Isar/generic_target.ML	Thu Aug 26 13:09:12 2010 +0200
     7.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Aug 26 15:48:08 2010 +0200
     7.3 @@ -195,16 +195,16 @@
     7.4        (Morphism.transform (Local_Theory.global_morphism lthy) decl);
     7.5    in
     7.6      lthy
     7.7 -    |> Local_Theory.theory (Context.theory_map global_decl)
     7.8 +    |> Local_Theory.background_theory (Context.theory_map global_decl)
     7.9      |> Local_Theory.target (Context.proof_map global_decl)
    7.10    end;
    7.11  
    7.12  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    7.13    let
    7.14 -    val (const, lthy2) = lthy |> Local_Theory.theory_result
    7.15 +    val (const, lthy2) = lthy |> Local_Theory.background_theory_result
    7.16        (Sign.declare_const ((b, U), mx));
    7.17      val lhs = list_comb (const, type_params @ term_params);
    7.18 -    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
    7.19 +    val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result
    7.20        (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
    7.21    in ((lhs, def), lthy3) end;
    7.22  
    7.23 @@ -214,12 +214,13 @@
    7.24      val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
    7.25    in
    7.26      lthy
    7.27 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
    7.28 +    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
    7.29      |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
    7.30    end;
    7.31  
    7.32 -fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
    7.33 -  (Sign.add_abbrev (#1 prmode) (b, t) #->
    7.34 -    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
    7.35 +fun theory_abbrev prmode ((b, mx), t) =
    7.36 +  Local_Theory.background_theory
    7.37 +    (Sign.add_abbrev (#1 prmode) (b, t) #->
    7.38 +      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
    7.39  
    7.40  end;

     8.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 26 13:09:12 2010 +0200
     8.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 26 15:48:08 2010 +0200
     8.3 @@ -21,8 +21,8 @@
     8.4    val target_of: local_theory -> Proof.context
     8.5    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     8.6    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     8.7 -  val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     8.8 -  val theory: (theory -> theory) -> local_theory -> local_theory
     8.9 +  val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    8.10 +  val background_theory: (theory -> theory) -> local_theory -> local_theory
    8.11    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    8.12    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    8.13    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
    8.14 @@ -144,7 +144,7 @@
    8.15  
    8.16  val checkpoint = raw_theory Theory.checkpoint;
    8.17  
    8.18 -fun theory_result f lthy =
    8.19 +fun background_theory_result f lthy =
    8.20    lthy |> raw_theory_result (fn thy =>
    8.21      thy
    8.22      |> Sign.map_naming (K (naming_of lthy))
    8.23 @@ -152,7 +152,7 @@
    8.24      ||> Sign.restore_naming thy
    8.25      ||> Theory.checkpoint);
    8.26  
    8.27 -fun theory f = #2 o theory_result (f #> pair ());
    8.28 +fun background_theory f = #2 o background_theory_result (f #> pair ());
    8.29  
    8.30  fun target_result f lthy =
    8.31    let
    8.32 @@ -169,7 +169,7 @@
    8.33  fun target f = #2 o target_result (f #> pair ());
    8.34  
    8.35  fun map_contexts f =
    8.36 -  theory (Context.theory_map f) #>
    8.37 +  background_theory (Context.theory_map f) #>
    8.38    target (Context.proof_map f) #>
    8.39    Context.proof_map f;
    8.40  

     9.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 26 13:09:12 2010 +0200
     9.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 26 15:48:08 2010 +0200
     9.3 @@ -497,8 +497,8 @@
     9.4  fun add_thmss loc kind args ctxt =
     9.5    let
     9.6      val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
     9.7 -    val ctxt'' = ctxt' |> ProofContext.background_theory (
     9.8 -      (change_locale loc o apfst o apsnd) (cons (args', serial ()))
     9.9 +    val ctxt'' = ctxt' |> ProofContext.background_theory
    9.10 +     ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
    9.11          #>
    9.12        (* Registrations *)
    9.13        (fn thy => fold_rev (fn (_, morph) =>

    10.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 26 13:09:12 2010 +0200
    10.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 26 15:48:08 2010 +0200
    10.3 @@ -118,7 +118,7 @@
    10.4        (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
    10.5    in
    10.6      lthy
    10.7 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
    10.8 +    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
    10.9      |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
   10.10    end
   10.11  
   10.12 @@ -129,19 +129,21 @@
   10.13  
   10.14  (* abbrev *)
   10.15  
   10.16 -fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
   10.17 -  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   10.18 -    (fn (lhs, _) => locale_const_declaration ta prmode
   10.19 -      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
   10.20 +fun locale_abbrev ta prmode ((b, mx), t) xs =
   10.21 +  Local_Theory.background_theory_result
   10.22 +    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   10.23 +      (fn (lhs, _) => locale_const_declaration ta prmode
   10.24 +        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
   10.25  
   10.26  fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
   10.27      prmode (b, mx) (global_rhs, t') xs lthy =
   10.28 -  if is_locale
   10.29 -    then lthy
   10.30 -      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
   10.31 -      |> is_class ? Class.abbrev target prmode ((b, mx), t')
   10.32 -    else lthy
   10.33 -      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
   10.34 +  if is_locale then
   10.35 +    lthy
   10.36 +    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
   10.37 +    |> is_class ? Class.abbrev target prmode ((b, mx), t')
   10.38 +  else
   10.39 +    lthy
   10.40 +    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
   10.41  
   10.42  
   10.43  (* pretty *)
   10.44 @@ -200,9 +202,10 @@
   10.45  
   10.46  fun init target thy = init_target (named_target thy target) thy;
   10.47  
   10.48 -fun reinit lthy = case peek lthy
   10.49 - of SOME {target, ...} => init target o Local_Theory.exit_global
   10.50 -  | NONE => error "Not in a named target";
   10.51 +fun reinit lthy =
   10.52 +  (case peek lthy of
   10.53 +    SOME {target, ...} => init target o Local_Theory.exit_global
   10.54 +  | NONE => error "Not in a named target");
   10.55  
   10.56  val theory_init = init_target global_target;
   10.57  

    11.1 --- a/src/Pure/Isar/overloading.ML	Thu Aug 26 13:09:12 2010 +0200
    11.2 +++ b/src/Pure/Isar/overloading.ML	Thu Aug 26 15:48:08 2010 +0200
    11.3 @@ -140,7 +140,7 @@
    11.4    end
    11.5  
    11.6  fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
    11.7 -  Local_Theory.theory_result
    11.8 +  Local_Theory.background_theory_result
    11.9      (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   11.10    ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   11.11    ##> Local_Theory.target synchronize_syntax

    12.1 --- a/src/Pure/Isar/typedecl.ML	Thu Aug 26 13:09:12 2010 +0200
    12.2 +++ b/src/Pure/Isar/typedecl.ML	Thu Aug 26 15:48:08 2010 +0200
    12.3 @@ -34,7 +34,7 @@
    12.4  fun basic_decl decl (b, n, mx) lthy =
    12.5    let val name = Local_Theory.full_name lthy b in
    12.6      lthy
    12.7 -    |> Local_Theory.theory (decl name)
    12.8 +    |> Local_Theory.background_theory (decl name)
    12.9      |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
   12.10      |> Local_Theory.type_alias b name
   12.11      |> pair name

    13.1 --- a/src/Pure/Thy/thy_load.ML	Thu Aug 26 13:09:12 2010 +0200
    13.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Aug 26 15:48:08 2010 +0200
    13.3 @@ -195,7 +195,7 @@
    13.4        val _ = Context.>> Local_Theory.propagate_ml_env;
    13.5  
    13.6        val provide = provide (src_path, (path, id));
    13.7 -      val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
    13.8 +      val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
    13.9      in () end;
   13.10  
   13.11  fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);