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/Lifting/lifting_setup.ML
changeset 47534 06cc372a80ed
parent 47521 69f95ac85c3d
child 47535 0f94b02fda1c 
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:53:28 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:52:49 2012 +0200
@@ -136,7 +136,7 @@
       |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
         [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
       |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
-        [T_def RS @{thm typedef_right_total}])
+        [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
       |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
         [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
       |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
isabelle