# HG changeset patch
# User traytel
# Date 1395675216 -3600
# Node ID 9b32aafecec172f0eb6a662de6d396a3380b6c50
# Parent  251f60be62a7cef2f9fac7fd96a71dc64d02137b
made tactic more robust

diff -r 251f60be62a7 -r 9b32aafecec1 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 24 16:33:36 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 24 16:33:36 2014 +0100
@@ -819,12 +819,14 @@
         fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
         val unique = HOLogic.mk_Trueprop
           (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
-        val unique_mor = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
-            (Logic.list_implies (prems @ mor_prems, unique)))
-          (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
-            in_mono'_thms alg_set_thms morE_thms map_cong0s))
-          |> Thm.close_derivation;
+        val cts = map (certify lthy) ss;
+        val unique_mor = singleton (Proof_Context.export names_lthy lthy)
+          (Goal.prove_sorry lthy [] []
+            (fold_rev Logic.all (init_xs @ Bs @ init_fs @ init_fs_copy)
+              (Logic.list_implies (prems @ mor_prems, unique)))
+            (K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
+              in_mono'_thms alg_set_thms morE_thms map_cong0s))
+          |> Thm.close_derivation);
       in
         split_conj_thm unique_mor
       end;
@@ -951,7 +953,7 @@
           |> Thm.close_derivation;
 
         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
-        val cts = map3 (SOME o certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+        val cts = map3 (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
diff -r 251f60be62a7 -r 9b32aafecec1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Mar 24 16:33:36 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Mar 24 16:33:36 2014 +0100
@@ -28,8 +28,8 @@
   val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
     tactic
   val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
-  val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> tactic
+  val mk_init_unique_mor_tac: cterm list -> int -> thm -> thm -> thm list -> thm list -> thm list ->
+    thm list -> thm list -> tactic
   val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
@@ -46,8 +46,8 @@
   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   val mk_min_algs_tac: thm -> thm list -> tactic
-  val mk_mor_Abs_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
-    thm list -> tactic
+  val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list ->
+    tactic
   val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
     thm list list -> tactic
   val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
@@ -349,7 +349,7 @@
       etac mor_comp, rtac mor_incl, REPEAT_DETERM_N n o rtac subset_UNIV] 1
   end;
 
-fun mk_init_unique_mor_tac m
+fun mk_init_unique_mor_tac cts m
     alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
   let
     val n = length least_min_algs;
@@ -358,21 +358,23 @@
     fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
       REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
       REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
-    fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
+    fun cong_tac ct map_cong0 = EVERY'
+      [rtac (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
       REPEAT_DETERM_N m o rtac refl,
       REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
 
-    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
-      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
-      REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
-      rtac trans, mor_tac morE in_mono,
-      rtac trans, cong_tac map_cong0,
-      rtac sym, mor_tac morE in_mono];
+    fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
+      EVERY' [rtac ballI, rtac CollectI,
+        REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
+        REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
+        rtac trans, mor_tac morE in_mono,
+        rtac trans, cong_tac ct map_cong0,
+        rtac sym, mor_tac morE in_mono];
 
     fun mk_unique_tac (k, least_min_alg) =
       select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
       rtac (alg_def RS iffD2) THEN'
-      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
+      CONJ_WRAP' mk_alg_tac (cts ~~ (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s))));
   in
     CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
   end;
@@ -414,7 +416,7 @@
     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
     CONJ_WRAP' (fn (ct, thm) =>
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
-        rtac (thm RS (cterm_instantiate_pos [NONE, NONE, ct] arg_cong) RS sym),
+        rtac (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
         EVERY' (map (fn Abs_inverse =>
           EVERY' [rtac (o_apply RS trans RS ballI), etac (set_mp RS Abs_inverse), atac])
         Abs_inverses)])