--- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Mar 06 13:44:01 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Mar 06 14:38:54 2014 +0100
@@ -535,9 +535,9 @@
val ctxt = Proof_Context.init_global thy9;
val case_combs =
- map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names;
+ map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names;
val constrss = map (fn (dtname, {descr, index, ...}) =>
- map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst)
+ map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst)
(#3 (the (AList.lookup op = descr index)))) dt_infos;
in
thy9