--- 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]),
--- 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);