--- a/src/Pure/Isar/specification.ML Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Isar/specification.ML Thu Mar 06 12:10:19 2014 +0100
@@ -276,7 +276,8 @@
in
val type_notation = gen_type_notation (K I);
-val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
+val type_notation_cmd =
+ gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = false, strict = false});
val notation = gen_notation (K I);
val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);