--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200
@@ -898,7 +898,7 @@
val goal = mk_parametricity_goal ctxt (Rs @ [R]) const constB;
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
rel_eqs transfers))
|> Thm.close_derivation
@@ -917,7 +917,7 @@
val goal = HOLogic.mk_Trueprop (mk_rel_fun Rfp_rel (Rpre_rel $ Rfp_rel) $ dtor $ dtorB);
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_dtor_transfer_tac ctxt dtor_rel_thm))
|> Thm.close_derivation
end;
@@ -942,7 +942,7 @@
|> HOLogic.mk_Trueprop;
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
|> Thm.close_derivation
end;
@@ -955,7 +955,7 @@
|> HOLogic.mk_Trueprop;
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
|> Thm.close_derivation
end;
@@ -973,7 +973,7 @@
val goal = HOLogic.mk_Trueprop (mk_rel_fun (Rpre_rel' $ RRssig_rel) RRssig_rel $ sctr $ sctrB);
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
|> Thm.close_derivation
end;
@@ -998,7 +998,7 @@
|> HOLogic.mk_Trueprop;
in
Variable.add_free_names ctxt goal []
- |> (fn vars => Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
+ |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
transfers))
|> Thm.close_derivation