renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -91,7 +91,7 @@
       | _ => (pair ts, K I))
 
     val discharge = fold (Boogie_VCs.discharge o pair vc_name)
-    fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
+    fun after_qed [thms] = ProofContext.background_theory (discharge (vcs ~~ thms))
       | after_qed _ = I
   in
     ProofContext.init_global thy

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -428,7 +428,7 @@
           unflat rules (map Drule.zero_var_indexes_list raw_thms);
             (*FIXME somehow dubious*)
       in
-        ProofContext.theory_result
+        ProofContext.background_theory_result
           (prove_rep_datatype config dt_names alt_names descr vs
             raw_inject half_distinct raw_induct)
         #-> after_qed

--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -70,7 +70,7 @@
   | NONE => raise NotFound
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
-fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo)  (* FIXME *)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute
   (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))

--- a/src/HOL/Tools/choice_specification.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -220,8 +220,8 @@
                     |> process_all (zip3 alt_names rew_imps frees)
             end
 
-      fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
-        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
+      fun after_qed [[thm]] = ProofContext.background_theory (fn thy =>
+        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
       |> ProofContext.init_global

--- a/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -326,7 +326,7 @@
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof";
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
@@ -337,7 +337,7 @@
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof";
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 

--- a/src/Pure/Isar/class.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/class.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -368,7 +368,7 @@
 fun gen_classrel mk_prop classrel thy =
   let
     fun after_qed results =
-      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
+      ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
   in
     thy
     |> ProofContext.init_global
@@ -608,7 +608,7 @@
     val (tycos, vs, sort) = read_multi_arity thy raw_arities;
     val sorts = map snd vs;
     val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
-    fun after_qed results = ProofContext.theory
+    fun after_qed results = ProofContext.background_theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy

--- a/src/Pure/Isar/class_declaration.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -330,7 +330,7 @@
     val some_prop = try the_single props;
     val some_dep_morph = try the_single (map snd deps);
     fun after_qed some_wit =
-      ProofContext.theory (Class.register_subclass (sub, sup)
+      ProofContext.background_theory (Class.register_subclass (sub, sup)
         some_dep_morph some_wit export)
       #> ProofContext.theory_of #> Named_Target.init sub;
   in do_proof after_qed some_prop goal_ctxt end;

--- a/src/Pure/Isar/expression.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -824,7 +824,7 @@
     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.theory o Context.theory_map)
+    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;
@@ -872,7 +872,7 @@
     val target = intern thy raw_target;
     val target_ctxt = Named_Target.init target thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-    fun after_qed witss = ProofContext.theory
+    fun after_qed witss = ProofContext.background_theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
         target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
   in Element.witness_proof after_qed propss goal_ctxt end;

--- a/src/Pure/Isar/local_theory.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -261,7 +261,7 @@
 
 (* exit *)
 
-val exit = ProofContext.theory Theory.checkpoint o operation #exit;
+val exit = ProofContext.background_theory Theory.checkpoint o operation #exit;
 val exit_global = ProofContext.theory_of o exit;
 
 fun exit_result f (x, lthy) =

--- a/src/Pure/Isar/locale.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -497,7 +497,7 @@
 fun add_thmss loc kind args ctxt =
   let
     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
-    val ctxt'' = ctxt' |> ProofContext.theory (
+    val ctxt'' = ctxt' |> ProofContext.background_theory (
       (change_locale loc o apfst o apsnd) (cons (args', serial ()))
         #>
       (* Registrations *)
@@ -519,7 +519,7 @@
       [([Drule.dummy_thm], [])])];
 
 fun add_syntax_declaration loc decl =
-  ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+  ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   #> add_declaration loc decl;
 
 

--- a/src/Pure/Isar/proof_context.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -38,8 +38,8 @@
   val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
   val transfer_syntax: theory -> Proof.context -> Proof.context
   val transfer: theory -> Proof.context -> Proof.context
-  val theory: (theory -> theory) -> Proof.context -> Proof.context
-  val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
+  val background_theory: (theory -> theory) -> Proof.context -> Proof.context
+  val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
@@ -283,9 +283,9 @@
 
 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
 
-fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
+fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
 
-fun theory_result f ctxt =
+fun background_theory_result f ctxt =
   let val (res, thy') = f (theory_of ctxt)
   in (res, ctxt |> transfer thy') end;