# HG changeset patch
# User blanchet
# Date 1388742528 -3600
# Node ID 494fd4ec38500c749db19c8dbc5f7a8145fe503e
# Parent  862c36b6e57ce231d11d93f676745a78c9002676
tuning

diff -r 862c36b6e57c -r 494fd4ec3850 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Jan 02 23:44:31 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Jan 03 10:48:48 2014 +0100
@@ -56,18 +56,16 @@
     Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
   | _ => Conv.concl_conv ~1 cv ct);
 
-fun inst_as_projs ctxt k thm =
+fun co_induct_inst_as_projs ctxt k thm =
   let
-    val fs =
-      Term.add_vars (prop_of thm) []
+    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 ctxt (Var f), certify ctxt (mk_proj T k))) fs;
+    val cfs = map (fn f as (_, T) => (certify ctxt (Var f), certify ctxt (mk_proj T k))) fs;
   in
     Drule.cterm_instantiate cfs thm
   end;
 
-val inst_as_projs_tac = PRIMITIVE oo inst_as_projs;
+val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
 
 fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
   unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
@@ -136,8 +134,8 @@
 
 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss =
   let val n = Integer.sum ns in
-    unfold_thms_tac ctxt ctr_defs THEN
-    HEADGOAL (rtac ctor_induct' THEN' inst_as_projs_tac ctxt) THEN
+    unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN
+    co_induct_inst_as_projs_tac ctxt 1 THEN
     EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_maps) pre_set_defss
       mss (unflat mss (1 upto n)) kkss)
   end;
@@ -167,10 +165,10 @@
     discss selss =
   let val ks = 1 upto n in
     EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk,
-        dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (HEADGOAL (inst_as_projs_tac ctxt)),
+        dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1),
         hyp_subst_tac ctxt] @
       map4 (fn k => fn ctr_def => fn discs => fn sels =>
-        EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
+        EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 2)] @
           map2 (fn k' => fn discs' =>
             if k' = k then
               mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels