# HG changeset patch
# User blanchet
# Date 1410177826 -7200
# Node ID 622daea5b925f82c8be77f8f8740304679b72ea0
# Parent  ba7a2d19880c691ab181ac2699951e5313053763
made SML/NJ happire

diff -r ba7a2d19880c -r 622daea5b925 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 14:03:40 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 14:03:46 2014 +0200
@@ -1068,9 +1068,9 @@
 
 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
 
-type ctr_options = (string -> bool) * bool
+type ctr_options = (string -> bool) * bool;
 
-val default_ctr_options = (K true, false);
+val default_ctr_options = (K true, false) : ctr_options;
 
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1