src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

         THEN trace_tac ctxt options "before single intro rule"
         THEN Subgoal.FOCUS_PREMS
            (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
         THEN (resolve_tac ctxt [if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}] 1)
     | prove_prems out_ts ((p, deriv) :: ps) =