--- a/src/Pure/Isar/locale.ML Sun Aug 30 23:34:24 2015 +0200
+++ b/src/Pure/Isar/locale.ML Mon Aug 31 05:12:14 2015 +0200
@@ -575,15 +575,17 @@
fun add_thmss _ _ [] ctxt = ctxt
| add_thmss loc kind facts ctxt =
- ctxt
- |> Attrib.local_notes kind facts |> snd
- |> Proof_Context.background_theory
- ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
- (* Registrations *)
- (fn thy =>
- fold_rev (fn (_, morph) =>
- snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
- (registrations_of (Context.Theory thy) loc) thy));
+ let val facts0 = (map o apsnd o map o apfst o map) Thm.trim_context facts in
+ ctxt
+ |> Attrib.local_notes kind facts |> snd
+ |> Proof_Context.background_theory
+ ((change_locale loc o apfst o apsnd) (cons ((kind, facts0), serial ())) #>
+ (* Registrations *)
+ (fn thy =>
+ fold_rev (fn (_, morph) =>
+ snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
+ (registrations_of (Context.Theory thy) loc) thy))
+ end;
(* Declarations *)