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