# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 71aa74965bc977e033a2dd7128469bb8b0c3f38e
# Parent  9b72d207617b6986de8a75f7fbe72168b36c2f36
generalized tactic a bit

diff -r 9b72d207617b -r 71aa74965bc9 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -115,7 +115,6 @@
   val mk_sumTN_balanced: typ list -> typ
 
   val id_const: typ -> term
-  val id_abs: typ -> term
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
@@ -289,7 +288,6 @@
 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
 
 fun id_const T = Const (@{const_name id}, T --> T);
-fun id_abs T = Abs (Name.uu, T, Bound 0);
 
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
diff -r 9b72d207617b -r 71aa74965bc9 src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -42,18 +42,20 @@
 
 val sum_prod_thms_rel = @{thms prod.cases prod_rel_def sum.cases sum_rel_def};
 
-fun inst_spurious_fs lthy thm =
+fun mk_proj n k T = funpow n (fn t => Abs (Name.uu, T, t)) (Bound (n - k));
+
+fun inst_as_projs ctxt n k thm =
   let
     val fs =
       Term.add_vars (prop_of thm) []
       |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
     val cfs =
-      map (fn f as (_, T) => (certify lthy (Var f), certify lthy (id_abs (domain_type T)))) fs;
+      map (fn f as (_, T) => (certify ctxt (Var f), certify ctxt (mk_proj n k (domain_type T)))) fs;
   in
     Drule.cterm_instantiate cfs thm
   end;
 
-val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
+val inst_as_projs_tac = PRIMITIVE ooo inst_as_projs;
 
 fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor =
   unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
@@ -132,7 +134,7 @@
     val nn = length ns;
     val n = Integer.sum ns;
   in
-    unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
+    unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_as_projs_tac ctxt 1 1 THEN
     EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
       pre_set_defss mss (unflat mss (1 upto n)) kkss)
   end;