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/Function/function.ML
changeset 78095 bc42c074e58f
parent 71214 5727bcc3c47c 
--- a/src/HOL/Tools/Function/function.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue May 23 18:46:15 2023 +0200
@@ -129,7 +129,7 @@
             (K false) (map fst fixes)
       in
         (info,
-         lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false}
+         lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
           (fn phi => add_function_data (transform_function_data phi info)))
       end
   in
@@ -209,7 +209,7 @@
           in
             (info',
              lthy2
-             |> Local_Theory.declaration {syntax = false, pervasive = false}
+             |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
                (fn phi => add_function_data (transform_function_data phi info'))
              |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
           end)
isabelle