author | blanchet |
Wed, 12 Feb 2014 08:35:56 +0100 | |
changeset 55407 | 81f7e60755c3 |
parent 55406 | 186076d100d3 |
child 55408 | 479a779b89a6 |
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 12 08:35:56 2014 +0100 @@ -439,7 +439,7 @@ val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = if no_discs_sels then - (true, [], [], [], [], [], lthy) + (true, [], [], [], [], [], lthy') else let fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);