src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 56806 f7d0520e7be2
parent 56805 8a87502c7da3
child 56858 0c3d0bc98abe
equal deleted inserted replaced
56805:8a87502c7da3 56806:f7d0520e7be2
   688         apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos
   688         apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos
   689           (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
   689           (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
   690 
   690 
   691     val sel_concls = sels ~~ ctr_args
   691     val sel_concls = sels ~~ ctr_args
   692       |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg))
   692       |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg))
   693         handle UnequalLengths =>
   693         handle ListPair.UnequalLengths =>
   694           primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
   694           primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
   695 
   695 
   696 (*
   696 (*
   697 val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} concl ^ "\nto\n    \<cdot> " ^
   697 val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} concl ^ "\nto\n    \<cdot> " ^
   698  (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n    \<cdot> ")) "" ^
   698  (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n    \<cdot> ")) "" ^