src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55407 81f7e60755c3
parent 55394 d5ebe055b599
child 55409 b74248961819
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -439,7 +439,7 @@
     1.4  
     1.5      val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
     1.6        if no_discs_sels then
     1.7 -        (true, [], [], [], [], [], lthy)
     1.8 +        (true, [], [], [], [], [], lthy')
     1.9        else
    1.10          let
    1.11            fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);