# HG changeset patch
# User bulwahn
# Date 1481206878 -3600
# Node ID c7d76708379f2d5468a14ea5ec39b53b45ed3c9f
# Parent  3d4331b658613805a57bd86fbdd7de33f6ef296b
filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)

diff -r 3d4331b65861 -r c7d76708379f src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Dec 07 08:14:40 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Dec 08 15:21:18 2016 +0100
@@ -125,6 +125,14 @@
 
 code_pred predicate_where_argument_is_neg_condition_and_in_equation .
 
+text {* Another related example that required slight adjustment of the proof procedure *}
+
+inductive if_as_predicate :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  "condition \<Longrightarrow> if_as_predicate condition then_value else_value then_value"
+| "\<not> condition \<Longrightarrow> if_as_predicate condition then_value else_value else_value"
+
+code_pred [show_proof_trace] if_as_predicate .
 
 inductive zerozero :: "nat * nat => bool"
 where
diff -r 3d4331b65861 -r c7d76708379f src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Dec 07 08:14:40 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Dec 08 15:21:18 2016 +0100
@@ -152,6 +152,7 @@
              THEN TRY (
                 let
                   val prems' = maps dest_conjunct_prem (take nargs prems)
+                    |> filter is_equationlike
                 in
                   rewrite_goal_tac ctxt'
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1