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

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

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

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

     5.1 --- a/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 12:06:00 2010 +0200
     5.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Thu Aug 26 13:09:12 2010 +0200
     5.3 @@ -326,7 +326,7 @@
     5.4      val args = map (apsnd (prep_constraint ctxt)) raw_args;
     5.5      val (goal1, goal2, make_result) =
     5.6        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     5.7 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
     5.8 +    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
     5.9        | after_qed _ = raise Fail "cpodef_proof";
    5.10    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    5.11  
    5.12 @@ -337,7 +337,7 @@
    5.13      val args = map (apsnd (prep_constraint ctxt)) raw_args;
    5.14      val (goal1, goal2, make_result) =
    5.15        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
    5.16 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
    5.17 +    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
    5.18        | after_qed _ = raise Fail "pcpodef_proof";
    5.19    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    5.20  

     6.1 --- a/src/Pure/Isar/class.ML	Thu Aug 26 12:06:00 2010 +0200
     6.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 26 13:09:12 2010 +0200
     6.3 @@ -368,7 +368,7 @@
     6.4  fun gen_classrel mk_prop classrel thy =
     6.5    let
     6.6      fun after_qed results =
     6.7 -      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
     6.8 +      ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
     6.9    in
    6.10      thy
    6.11      |> ProofContext.init_global
    6.12 @@ -608,7 +608,7 @@
    6.13      val (tycos, vs, sort) = read_multi_arity thy raw_arities;
    6.14      val sorts = map snd vs;
    6.15      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    6.16 -    fun after_qed results = ProofContext.theory
    6.17 +    fun after_qed results = ProofContext.background_theory
    6.18        ((fold o fold) AxClass.add_arity results);
    6.19    in
    6.20      thy

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

     8.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 26 12:06:00 2010 +0200
     8.2 +++ b/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
     8.3 @@ -824,7 +824,7 @@
     8.4      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     8.5      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
     8.6  
     8.7 -    fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
     8.8 +    fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
     8.9        (note_eqns_register deps witss attrss eqns export export');
    8.10  
    8.11    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    8.12 @@ -872,7 +872,7 @@
    8.13      val target = intern thy raw_target;
    8.14      val target_ctxt = Named_Target.init target thy;
    8.15      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    8.16 -    fun after_qed witss = ProofContext.theory
    8.17 +    fun after_qed witss = ProofContext.background_theory
    8.18        (fold (fn ((dep, morph), wits) => Locale.add_dependency
    8.19          target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
    8.20    in Element.witness_proof after_qed propss goal_ctxt end;

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

    10.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 26 12:06:00 2010 +0200
    10.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 26 13:09:12 2010 +0200
    10.3 @@ -497,7 +497,7 @@
    10.4  fun add_thmss loc kind args ctxt =
    10.5    let
    10.6      val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
    10.7 -    val ctxt'' = ctxt' |> ProofContext.theory (
    10.8 +    val ctxt'' = ctxt' |> ProofContext.background_theory (
    10.9        (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   10.10          #>
   10.11        (* Registrations *)
   10.12 @@ -519,7 +519,7 @@
   10.13        [([Drule.dummy_thm], [])])];
   10.14  
   10.15  fun add_syntax_declaration loc decl =
   10.16 -  ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   10.17 +  ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   10.18    #> add_declaration loc decl;
   10.19  
   10.20  

    11.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 26 12:06:00 2010 +0200
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 26 13:09:12 2010 +0200
    11.3 @@ -38,8 +38,8 @@
    11.4    val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
    11.5    val transfer_syntax: theory -> Proof.context -> Proof.context
    11.6    val transfer: theory -> Proof.context -> Proof.context
    11.7 -  val theory: (theory -> theory) -> Proof.context -> Proof.context
    11.8 -  val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    11.9 +  val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   11.10 +  val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   11.11    val extern_fact: Proof.context -> string -> xstring
   11.12    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   11.13    val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   11.14 @@ -283,9 +283,9 @@
   11.15  
   11.16  fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
   11.17  
   11.18 -fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
   11.19 +fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
   11.20  
   11.21 -fun theory_result f ctxt =
   11.22 +fun background_theory_result f ctxt =
   11.23    let val (res, thy') = f (theory_of ctxt)
   11.24    in (res, ctxt |> transfer thy') end;
   11.25