# HG changeset patch
# User blanchet
# Date 1389363060 -3600
# Node ID 451786451d040e4e851af4d43808f4251f0c866a
# Parent  d1c76303244eb37eda750ac6349544edb85d837d
pass right rhs as code rhs

diff -r d1c76303244e -r 451786451d04 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:58:31 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 15:11:00 2014 +0100
@@ -712,7 +712,8 @@
     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