--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Tue Dec 13 23:29:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Wed Dec 14 09:19:49 2016 +0100
@@ -156,7 +156,8 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt [rel_def] THEN
- HEADGOAL (rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
+ HEADGOAL (rtac ctxt refl ORELSE'
+ rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
end
end;
@@ -178,7 +179,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt [rel_def] THEN
- HEADGOAL (rtac ctxt @{thm vimage2p_rel_fun})))
+ HEADGOAL (rtac ctxt refl ORELSE' rtac ctxt @{thm vimage2p_rel_fun})))
end
end;