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/Transfer/transfer_bnf.ML
changeset 58458 0c9d59cb3af9
parent 58356 2f04f1fd28aa
child 58659 6c9821c32dd5 
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Sep 26 14:36:54 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Sep 26 14:41:08 2014 +0200
@@ -348,7 +348,7 @@
             else thm RS (@{thm eq_onp_same_args} RS iffD1))
         |> kill_top
       end
-    val rel_injects = #rel_injects fp_sugar
+    val rel_injects = #rel_injects (#fp_bnf_sugar fp_sugar)
   in
     rel_injects
     |> map (Local_Defs.unfold lthy [@{thm conj_assoc}])
isabelle