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/HOL/Tools/functor.ML
changeset 78095 bc42c074e58f
parent 74561 8e6c973003c8
child 80634 a90ab1ea6458 
--- a/src/HOL/Tools/functor.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/functor.ML	Tue May 23 18:46:15 2023 +0200
@@ -263,7 +263,7 @@
         |> Local_Theory.note ((qualify identityN, []),
             [prove_identity lthy id_thm])
         |> snd
-        |> Local_Theory.declaration {syntax = false, pervasive = false}
+        |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
           (mapper_declaration comp_thm id_thm))
   in
     lthy
isabelle