Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 18 Jan 2021 13:43:32 +0100
changeset 73147 cc71193891c2
parent 73146 9dafcf6f152b
child 73148 5f49f1149c1c
tuned;
src/Pure/Thy/bibtex.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/bibtex.ML	Mon Jan 18 13:41:54 2021 +0100
+++ b/src/Pure/Thy/bibtex.ML	Mon Jan 18 13:43:32 2021 +0100
@@ -46,10 +46,10 @@
         (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
       (fn ctxt => fn (opt, citations) =>
         let
-          val thy = Proof_Context.theory_of ctxt;
-          val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy);
+          val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
+          val bibtex_entries = Resources.theory_bibtex_entries thy_name;
           val _ =
-            if null bibtex_entries andalso Context.theory_long_name thy <> Context.PureN then ()
+            if null bibtex_entries andalso thy_name <> Context.PureN then ()
             else
               citations |> List.app (fn (name, pos) =>
                 if member (op =) bibtex_entries name then ()
isabelle