src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

--- 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);