src/Pure/Isar/specification.ML

   lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
 
 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);
 
 end;