robustness
authorblanchet
Wed Dec 14 09:19:49 2016 +0100 (2016-12-14)
changeset 6455863c76802ab5e
parent 64557 37074e22e8be
child 64559 abd9a9fd030b
robustness
src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Dec 13 23:29:54 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Wed Dec 14 09:19:49 2016 +0100
     1.3 @@ -156,7 +156,8 @@
     1.4          Variable.add_free_names ctxt goal []
     1.5          |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
     1.6            unfold_thms_tac ctxt [rel_def] THEN
     1.7 -          HEADGOAL (rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
     1.8 +          HEADGOAL (rtac ctxt refl ORELSE'
     1.9 +            rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
    1.10        end
    1.11    end;
    1.12  
    1.13 @@ -178,7 +179,7 @@
    1.14          Variable.add_free_names ctxt goal []
    1.15          |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
    1.16            unfold_thms_tac ctxt [rel_def] THEN
    1.17 -          HEADGOAL (rtac ctxt @{thm vimage2p_rel_fun})))
    1.18 +          HEADGOAL (rtac ctxt refl ORELSE' rtac ctxt @{thm vimage2p_rel_fun})))
    1.19        end
    1.20    end;
    1.21