--- a/src/HOL/Tools/Datatype/rep_datatype.ML Sun Mar 09 15:21:08 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sun Mar 09 16:37:56 2014 +0100
@@ -535,9 +535,9 @@
val ctxt = Proof_Context.init_global thy9;
val case_combs =
- map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
+ map (Proof_Context.read_const {proper = true, strict = true} ctxt) case_names;
val constrss = map (fn (dtname, {descr, index, ...}) =>
- map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
+ map (Proof_Context.read_const {proper = true, strict = true} ctxt o fst)
(#3 (the (AList.lookup op = descr index)))) dt_infos;
in
thy9