1.1 --- a/src/Pure/Isar/named_target.ML Mon Sep 20 15:29:53 2010 +0200
1.2 +++ b/src/Pure/Isar/named_target.ML Mon Sep 20 16:05:25 2010 +0200
1.3 @@ -118,7 +118,7 @@
1.4 (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
1.5 in
1.6 lthy
1.7 - |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
1.8 + |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
1.9 |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
1.10 end
1.11