Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/generic_target.ML
changeset 79368 a2d8ecb13d3f
parent 79359 5b01b93de062
child 79371 a2fbac74fba7 
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -366,7 +366,7 @@
     val (facts', lthy') =
       (facts, lthy) |-> fold_map (fn (a, thms) => fn lthy1 =>
         let
-          val thms1 = name_thms (Local_Theory.bind_name lthy1 (fst a)) thms;
+          val thms1 = name_thms (Local_Theory.full_name_pos lthy1 (fst a)) thms;
           val (thms2, lthy2) =
             (thms1, lthy1) |-> fold_map (fn (args, atts) =>
               fold_map thm_definition args #>> rpair atts);
isabelle