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 71214 5727bcc3c47c
parent 71179 592e2afdd50c
child 78095 bc42c074e58f 
--- a/src/HOL/Tools/Function/function.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -211,7 +211,7 @@
              lthy2
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => add_function_data (transform_function_data phi info'))
-             |> Spec_Rules.add "" Spec_Rules.equational_recdef fs tsimps)
+             |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
           end)
       end
   in
isabelle