merged

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Jan 10 20:29:12 2016 -0800
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Jan 11 07:44:20 2016 +0100
@@ -85,10 +85,47 @@
 
 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-"Fact a' a'"
+  "Fact a' a'"
 
 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
 
+text {*
+  The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
+*}
+inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
+where
+  "ck \<Longrightarrow> predicate_where_argument_is_condition ck"
+
+code_pred predicate_where_argument_is_condition .
+
+text {* Other similar examples of this kind: *}
+
+inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
+where
+  "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
+
+code_pred predicate_where_argument_is_in_equation .
+
+inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
+where
+  "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
+     \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"
+
+code_pred predicate_where_argument_is_condition_and_value .
+
+inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
+where
+  "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
+
+code_pred predicate_where_argument_is_neg_condition .
+
+inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
+where
+  "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
+
+code_pred predicate_where_argument_is_neg_condition_and_in_equation .
+
+
 inductive zerozero :: "nat * nat => bool"
 where
   "zerozero (0, 0)"

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Jan 10 20:29:12 2016 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Jan 11 07:44:20 2016 +0100
@@ -195,6 +195,7 @@
            (fn {context = ctxt', prems, ...} =>
             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
             end) ctxt 1