# HG changeset patch
# User traytel
# Date 1395675216 -3600
# Node ID 251f60be62a7cef2f9fac7fd96a71dc64d02137b
# Parent  918432e3fcfa6d48a8e2a77fc88e4f624979c80f
inline helper function

diff -r 918432e3fcfa -r 251f60be62a7 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Mar 24 14:22:29 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Mar 24 16:33:36 2014 +0100
@@ -535,8 +535,9 @@
       rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
 
     fun mk_set_nat cset ctor_map ctor_set set_nats =
-      EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
-        rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
+      EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl, rtac sym,
+        rtac (trans OF [ctor_map RS cterm_instantiate_pos [NONE, NONE, SOME cset] arg_cong,
+          ctor_set RS trans]),
         rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
         rtac sym, rtac (nth set_nats (i - 1)),
         REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
diff -r 918432e3fcfa -r 251f60be62a7 src/HOL/Tools/BNF/bnf_lfp_util.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML	Mon Mar 24 14:22:29 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML	Mon Mar 24 16:33:36 2014 +0100
@@ -8,8 +8,6 @@
 
 signature BNF_LFP_UTIL =
 sig
-  val HOL_arg_cong: cterm -> thm
-
   val mk_bij_betw: term -> term -> term -> term
   val mk_cardSuc: term -> term
   val mk_not_empty: term -> term
@@ -25,9 +23,6 @@
 
 open BNF_Util
 
-fun HOL_arg_cong ct = Drule.instantiate'
-  (map SOME (Thm.dest_ctyp (Thm.ctyp_of_term ct))) [NONE, NONE, SOME ct] arg_cong;
-
 (*reverse application*)
 fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg);