# HG changeset patch
# User traytel
# Date 1477320812 -7200
# Node ID e9eb0b99a44cb9a3935b627cebb14d28f4321f0a
# Parent  c1db9e3fe0e2356940c8257d86c840db697e8389
apply transfer_prover after folding relator_eq

diff -r c1db9e3fe0e2 -r e9eb0b99a44c src/HOL/Library/BNF_Corec.thy
--- a/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:16:55 2016 +0200
+++ b/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:53:32 2016 +0200
@@ -206,6 +206,10 @@
 ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
 ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
 
+method_setup transfer_prover_eq = \<open>
+  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
+\<close> "apply transfer_prover after folding relator_eq"
+
 method_setup corec_unique = \<open>
   Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
 \<close> "prove uniqueness of corecursive equation"
diff -r c1db9e3fe0e2 -r e9eb0b99a44c src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML	Mon Oct 24 16:16:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML	Mon Oct 24 16:53:32 2016 +0200
@@ -8,6 +8,7 @@
 
 signature BNF_GFP_GREC_TACTICS =
 sig
+  val transfer_prover_eq_tac: Proof.context -> int -> tactic
   val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic
 
   val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
@@ -82,8 +83,12 @@
     rel_eqs ctxt;
 val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]);
 
+fun transfer_prover_eq_tac ctxt =
+  SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN'
+  Transfer.transfer_prover_tac ctxt;
+
 fun transfer_prover_add_tac ctxt rel_eqs transfers =
-  Transfer.transfer_prover_tac (ctxt
+  transfer_prover_eq_tac (ctxt
     |> context_relator_eq_add rel_eqs
     |> context_transfer_rule_add transfers);