# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID b0bf94ccc59fd601638bd31a2255bc0668903ca0
# Parent  6401e2d5e68f3f9ce916cf489cc0912016b18db5
avoid 'prove_sorry' for unreliable tactics

diff -r 6401e2d5e68f -r b0bf94ccc59f src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- 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
diff -r 6401e2d5e68f -r b0bf94ccc59f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -527,7 +527,7 @@
       (case Thm.prop_of thm of @{const Trueprop} $ (_ $ cst $ _) => cst);
 
     val eq_algrho =
-      Goal.prove_sorry (*FIXME*) (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
+      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse
           fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
           live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs
@@ -575,7 +575,7 @@
     val SOME {abs_rep_transfers, ...} = codatatype_extra_of ctxt fpT_name;
   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_rho_transfer_tac ctxt (null abs_rep_transfers) (rel_def_of_bnf pre_bnf)
       const_transfers))
     |> unfold_thms ctxt [rho_def RS @{thm symmetric}]
@@ -1163,7 +1163,6 @@
                 |> `(curry fastype_of1 bound_Ts)
                 |>> build_params bound_Us bound_Ts
                 |-> explore;
-              (* FIXME: This looks suspicious *)
               val Us = map (fpT_to ssig_T) (snd (dest_Type (fastype_of1 (bound_Us, mapped_arg'))));
               val temporary_map = map_tm
                 |> mk_map n Us Ts;
@@ -2179,7 +2178,7 @@
 
     fun prove_transfer_goal ctxt goal =
       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 = _} =>
         HEADGOAL (Transfer.transfer_prover_tac ctxt)))
       |> Thm.close_derivation;