# HG changeset patch
# User traytel
# Date 1472540680 -7200
# Node ID 2d21591967bc1733660bcff9482fa3e37863a1d4
# Parent  dd327befd2ef2ed9965d2d92d9aa7bfc34be1328
generate proper goal when equation is entered programmatically

diff -r dd327befd2ef -r 2d21591967bc src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Aug 29 21:46:24 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 30 09:04:40 2016 +0200
@@ -1454,6 +1454,7 @@
                     val ms = map (Logic.count_prems o Thm.prop_of) ctr_thms;
                     val (raw_goal, goal) = (raw_rhs, rhs)
                       |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
+                        #> abstract_over_list fun_args
                         #> curry Logic.list_all (map dest_Free fun_args));
                     val (distincts, discIs, _, split_sels, split_sel_asms) =
                       case_thms_of_term lthy raw_rhs;