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/BNF/bnf_comp.ML
changeset 58359 3782c7b0d1cc
parent 58332 be0f5d8d511b
child 58634 9f10d82e8188 
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 12:09:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 16:20:13 2014 +0200
@@ -837,7 +837,8 @@
       rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
     fun rel_OO_Grp_tac ctxt =
       (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
-       subst_tac ctxt NONE [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
+       (if has_live_phantoms then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt)
+         [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
        SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
          type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
          type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
isabelle