# HG changeset patch
# User blanchet
# Date 1380099189 -7200
# Node ID c25acff63bfe1070e85db2975cc783cdc67d4c05
# Parent  8ad44ecc0d1562b1e921b12c7c8308d2aecd7259
removed dead code

diff -r 8ad44ecc0d15 -r c25acff63bfe src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 10:45:12 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 10:53:09 2013 +0200
@@ -172,15 +172,6 @@
    (if b then f y else if b' then x' else f y')"
   by simp
 
-lemma if_then_else_True_False:
-  "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
-  "(if p then True else r) \<longleftrightarrow> p \<or> r"
-  "(if p then q else False) \<longleftrightarrow> p \<and> q"
-  "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
-by simp_all
-
-lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
-
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"
diff -r 8ad44ecc0d15 -r c25acff63bfe src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:45:12 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:53:09 2013 +0200
@@ -62,7 +62,6 @@
     term -> term
   val fold_rev_corec_code_rhs: Proof.context -> (term -> term list -> 'a -> 'a) -> typ list ->
     term -> 'a -> 'a
-  val simplify_bool_ifs: theory -> term -> term list
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -328,15 +327,6 @@
 
 fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
 
-fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
-  | add_conjuncts t = cons t;
-
-fun conjuncts t = add_conjuncts t [];
-
-fun simplify_bool_ifs thy =
-  Raw_Simplifier.rewrite_term thy @{thms bool_if_simps[THEN eq_reflection]} []
-  #> conjuncts #> (fn [@{term True}] => [] | ts => ts);
-
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
 fun indexedd xss = fold_map indexed xss;
 fun indexeddd xsss = fold_map indexedd xsss;