# HG changeset patch
# User blanchet
# Date 1381735024 -7200
# Node ID 94f2dc9aea7a28496b14ad33beecf16dedd93f11
# Parent  6fefbaeccb63dd7c65f6b4edb311fe68a695618f
strengthened tactic w.r.t. "let"

diff -r 6fefbaeccb63 -r 94f2dc9aea7a src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 13 21:36:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 14 09:17:04 2013 +0200
@@ -1015,14 +1015,11 @@
                 val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms
                   |> K |> Goal.prove lthy [] [] raw_t;
-val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
               in
-                mk_primcorec_code_of_raw_code_tac sel_splits raw_code_thm
+                mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
                 |> K |> Goal.prove lthy [] [] t
-|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
                 |> single
               end
-handle ERROR s => (warning s; []) (*###*)
           end;
 
         val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
diff -r 6fefbaeccb63 -r 94f2dc9aea7a src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 13 21:36:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Oct 14 09:17:04 2013 +0200
@@ -8,7 +8,7 @@
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
-  val mk_primcorec_code_of_raw_code_tac: thm list -> thm -> tactic
+  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
@@ -89,7 +89,8 @@
 
 (* TODO: reduce code duplication with selector tactic above *)
 fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
-  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
+  HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE'
+    Splitter.split_tac (split_if :: splits))) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
   HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
     SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
@@ -105,8 +106,9 @@
   EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
     ms ctr_thms);
 
-fun mk_primcorec_code_of_raw_code_tac splits raw =
-  HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
+fun mk_primcorec_code_of_raw_code_tac ctxt splits raw =
+  HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
+    SELECT_GOAL (unfold_thms_tac ctxt @{thms Let_def}) THEN' REPEAT_DETERM o
     (rtac refl ORELSE'
      (TRY o rtac sym) THEN' atac ORELSE'
      resolve_tac split_connectI ORELSE'