--- a/src/Pure/Isar/locale.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 27 12:57:55 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.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) =>
@@ -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;