--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Sat Sep 08 21:04:26 2012 +0200
@@ -8,6 +8,8 @@
signature BNF_TACTICS =
sig
+ val ss_only: thm list -> simpset
+
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> int -> tactic
val subst_asm_tac: Proof.context -> thm list -> int -> tactic
@@ -56,6 +58,8 @@
open BNF_Util
+fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
+
val set_mp = @{thm set_mp};
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,