# HG changeset patch
# User blanchet
# Date 1379515459 -7200
# Node ID 221ec353bcc566852a0f94398856e89ccc45fc1b
# Parent  ee9eaab634e5a3ebe6c515988f987cbc00b29ff7
minor change related to code equations in primcorec

diff -r ee9eaab634e5 -r 221ec353bcc5 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 16:09:15 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 16:44:19 2013 +0200
@@ -13,6 +13,11 @@
 imports BNF_Comp BNF_Ctr_Sugar
 begin
 
+definition code_unspec :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
+[code del]: "code_unspec f = f ()"
+
+code_abort code_unspec
+
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
 by auto
 
diff -r ee9eaab634e5 -r 221ec353bcc5 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 16:09:15 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 16:44:19 2013 +0200
@@ -8,7 +8,7 @@
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> tactic
+  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
   val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
     thm list list list -> thm list -> thm list -> thm list -> tactic
@@ -73,8 +73,7 @@
   REPEAT_DETERM_N 2 (HEADGOAL
     (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)));
 
-fun mk_primcorec_code_of_ctr_tac ctxt defs ctr_thms =
-  unfold_thms_tac ctxt defs THEN
+fun mk_primcorec_code_of_ctr_tac ctxt ctr_thms =
   EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt []) ctr_thms);
 
 fun mk_primcorec_code_tac ctxt raw collapses =