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