--- 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
--- 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 =