--- 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) =>