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/partial_function.ML
changeset 69992 bd3c10813cc4
parent 69829 3bfa28b3a5b2
child 70319 34bc296374ee 
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -302,7 +302,7 @@
     val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
   in
     lthy''
-    |> Spec_Rules.add Spec_Rules.Equational ([f], [rec_rule'])
+    |> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule'])
     |> note_qualified ("simps", [rec_rule'])
     |> note_qualified ("mono", [mono_thm])
     |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
isabelle