# HG changeset patch
# User blanchet
# Date 1413386288 -7200
# Node ID 6a75a4c24339df7d26f1b4177f7ecddcadee888d
# Parent  56b9eab818ca2d1217385c99abfac8834afdb451
made SML/NJ happier

diff -r 56b9eab818ca -r 6a75a4c24339 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 15 17:15:11 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 15 17:18:08 2014 +0200
@@ -128,10 +128,10 @@
    split_sel_asms: thm list,
    case_eq_ifs: thm list};
 
-fun morph_ctr_sugar phi {kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
+fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
     sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
-    split_sel_asms, case_eq_ifs} =
+    split_sel_asms, case_eq_ifs} : ctr_sugar) =
   {kind = kind,
    T = Morphism.typ phi T,
    ctrs = map (Morphism.term phi) ctrs,