# HG changeset patch
# User wenzelm
# Date 1282830488 -7200
# Node ID 2b3e054ae6fcfe37763fcfe035ec073d9d391c17
# Parent  d07959fabde63c794df8b4e586c6abe9b902df49
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

diff -r d07959fabde6 -r 2b3e054ae6fc src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -176,9 +176,9 @@
      val t = Const (const, T)
      val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
   in
-    if (is_inductify options) then
+    if is_inductify options then
       let
-        val lthy' = Local_Theory.theory (preprocess options t) lthy
+        val lthy' = Local_Theory.background_theory (preprocess options t) lthy
         val const =
           case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
             SOME c => c
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
diff -r d07959fabde6 -r 2b3e054ae6fc src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -77,7 +77,8 @@
   Typedef.add_typedef false NONE (qty_name, vs, mx) 
     (typedef_term rel rty lthy) NONE typedef_tac lthy
 *)
-   Local_Theory.theory_result
+(* FIXME should really use local typedef here *)
+   Local_Theory.background_theory_result
      (Typedef.add_typedef_global false NONE
        (qty_name, map (rpair dummyS) vs, mx)
          (typedef_term rel rty lthy)
diff -r d07959fabde6 -r 2b3e054ae6fc src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -186,7 +186,8 @@
           ||> Thm.term_of;
 
         val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
-          Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
+          Local_Theory.background_theory_result
+            (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
 
         val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
         val typedef =
@@ -246,7 +247,7 @@
       in
         lthy2
         |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
-        |> Local_Theory.theory (Typedef_Interpretation.data full_tname)
+        |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
         |> pair (full_tname, info)
       end;
 
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/class.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -482,7 +482,7 @@
 
 val type_name = sanitize_name o Long_Name.base_name;
 
-fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
     (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_inst_syntax;
@@ -572,7 +572,7 @@
     val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
     fun after_qed' results =
-      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
+      Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
       #> after_qed;
   in
     lthy
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -824,8 +824,9 @@
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
-    fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
-      (note_eqns_register deps witss attrss eqns export export');
+    fun after_qed witss eqns =
+      (ProofContext.background_theory o Context.theory_map)
+        (note_eqns_register deps witss attrss eqns export export');
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -195,16 +195,16 @@
       (Morphism.transform (Local_Theory.global_morphism lthy) decl);
   in
     lthy
-    |> Local_Theory.theory (Context.theory_map global_decl)
+    |> Local_Theory.background_theory (Context.theory_map global_decl)
     |> Local_Theory.target (Context.proof_map global_decl)
   end;
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
-    val (const, lthy2) = lthy |> Local_Theory.theory_result
+    val (const, lthy2) = lthy |> Local_Theory.background_theory_result
       (Sign.declare_const ((b, U), mx));
     val lhs = list_comb (const, type_params @ term_params);
-    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
+    val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result
       (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
@@ -214,12 +214,13 @@
     val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
   in
     lthy
-    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
     |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
   end;
 
-fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
-  (Sign.add_abbrev (#1 prmode) (b, t) #->
-    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+fun theory_abbrev prmode ((b, mx), t) =
+  Local_Theory.background_theory
+    (Sign.add_abbrev (#1 prmode) (b, t) #->
+      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
 
 end;
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -21,8 +21,8 @@
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
-  val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
-  val theory: (theory -> theory) -> local_theory -> local_theory
+  val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
+  val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
@@ -144,7 +144,7 @@
 
 val checkpoint = raw_theory Theory.checkpoint;
 
-fun theory_result f lthy =
+fun background_theory_result f lthy =
   lthy |> raw_theory_result (fn thy =>
     thy
     |> Sign.map_naming (K (naming_of lthy))
@@ -152,7 +152,7 @@
     ||> Sign.restore_naming thy
     ||> Theory.checkpoint);
 
-fun theory f = #2 o theory_result (f #> pair ());
+fun background_theory f = #2 o background_theory_result (f #> pair ());
 
 fun target_result f lthy =
   let
@@ -169,7 +169,7 @@
 fun target f = #2 o target_result (f #> pair ());
 
 fun map_contexts f =
-  theory (Context.theory_map f) #>
+  background_theory (Context.theory_map f) #>
   target (Context.proof_map f) #>
   Context.proof_map f;
 
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -497,8 +497,8 @@
 fun add_thmss loc kind args ctxt =
   let
     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
-    val ctxt'' = ctxt' |> ProofContext.background_theory (
-      (change_locale loc o apfst o apsnd) (cons (args', serial ()))
+    val ctxt'' = ctxt' |> ProofContext.background_theory
+     ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
         #>
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -118,7 +118,7 @@
       (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
   in
     lthy
-    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
     |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
   end
 
@@ -129,19 +129,21 @@
 
 (* abbrev *)
 
-fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
-  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
-    (fn (lhs, _) => locale_const_declaration ta prmode
-      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+fun locale_abbrev ta prmode ((b, mx), t) xs =
+  Local_Theory.background_theory_result
+    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
+      (fn (lhs, _) => locale_const_declaration ta prmode
+        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
     prmode (b, mx) (global_rhs, t') xs lthy =
-  if is_locale
-    then lthy
-      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
-      |> is_class ? Class.abbrev target prmode ((b, mx), t')
-    else lthy
-      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+  if is_locale then
+    lthy
+    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+    |> is_class ? Class.abbrev target prmode ((b, mx), t')
+  else
+    lthy
+    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
 
 
 (* pretty *)
@@ -200,9 +202,10 @@
 
 fun init target thy = init_target (named_target thy target) thy;
 
-fun reinit lthy = case peek lthy
- of SOME {target, ...} => init target o Local_Theory.exit_global
-  | NONE => error "Not in a named target";
+fun reinit lthy =
+  (case peek lthy of
+    SOME {target, ...} => init target o Local_Theory.exit_global
+  | NONE => error "Not in a named target");
 
 val theory_init = init_target global_target;
 
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -140,7 +140,7 @@
   end
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
-  Local_Theory.theory_result
+  Local_Theory.background_theory_result
     (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_syntax
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -34,7 +34,7 @@
 fun basic_decl decl (b, n, mx) lthy =
   let val name = Local_Theory.full_name lthy b in
     lthy
-    |> Local_Theory.theory (decl name)
+    |> Local_Theory.background_theory (decl name)
     |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
     |> Local_Theory.type_alias b name
     |> pair name
diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 26 15:48:08 2010 +0200
@@ -195,7 +195,7 @@
       val _ = Context.>> Local_Theory.propagate_ml_env;
 
       val provide = provide (src_path, (path, id));
-      val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
+      val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
     in () end;
 
 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);