# HG changeset patch
# User blanchet
# Date 1481703589 -3600
# Node ID 63c76802ab5e873782de75c20cd5571c826e290b
# Parent  37074e22e8be4e0596fcf6d5deea165176f1fa81
robustness

diff -r 37074e22e8be -r 63c76802ab5e src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
--- 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;