src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

       ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
        matchedsss)
     else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
       if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
         dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
-          (if null prems then SOME eqn0 else NONE) prems concl matchedsss
+          (if null prems then SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop eqn))) else NONE)
+          prems concl matchedsss
       else if null prems then
         dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
         |>> flat
       else
         primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn