--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
@@ -135,7 +135,7 @@
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
- fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
+ fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos;
(* complex queries *)