From a2ef4fbb01959b221392e01b9253b1ee988f522b Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 2 Jun 2016 11:56:25 +1000 Subject: [PATCH] add support for re-noting qualified facts with note_new_facts otherwise would fail if the sublocale contained "foo.simps", etc. --- lib/Extend_Locale.thy | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/lib/Extend_Locale.thy b/lib/Extend_Locale.thy index efa91a787..f4b3d93f8 100644 --- a/lib/Extend_Locale.thy +++ b/lib/Extend_Locale.thy @@ -26,15 +26,17 @@ let val space = Facts.space_of (Proof_Context.facts_of lthy); + fun make_binding (long_name, pos) = + let val (qualifier, name) = split_last (Long_Name.explode long_name) + in fold (Binding.qualify true) qualifier (Binding.make (name, pos)) end; + fun add_entry (nm, thms) lthy = - case Long_Name.dest_local nm of - SOME nm' => let + val extern_nm = Name_Space.extern_shortest lthy space nm; val {pos, ...} = Name_Space.the_entry space nm; - val b = Binding.make (nm', pos); + val b = make_binding (extern_nm, pos); val (_, lthy') = Local_Theory.note ((b,[]),thms) lthy; in lthy' end - | NONE => lthy; in fold add_entry local_facts lthy end; \