| changeset 47080 | bfad2f674d0e |
| parent 47069 | 451fc10a81f3 |
| child 47081 | 5e70b457b704 |
--- a/src/Pure/Isar/named_target.ML Thu Mar 22 10:49:31 2012 +0100 +++ b/src/Pure/Isar/named_target.ML Thu Mar 22 11:11:51 2012 +0100 @@ -133,7 +133,7 @@ lthy |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd) |> Local_Theory.target (Locale.add_thmss locale kind local_facts') - end + end; fun target_notes (Target {target, is_locale, ...}) = if is_locale then locale_notes target