more rigid type_name demands, based on educated guesses about the tools involved here;

--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:10:19 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:43:29 2014 +0100
@@ -185,7 +185,7 @@
      (Scan.succeed false);
 
 fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.type_name {proper = false, strict = true} >>
+  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
     (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
 fun setup_fresh_fun_simp x =

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:10:19 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:43:29 2014 +0100
@@ -234,7 +234,7 @@
 (** document antiquotation **)
 
 val antiq_setup =
-  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, strict = true})
+  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
     (fn {source = src, context = ctxt, ...} => fn dtco =>
       let
         val thy = Proof_Context.theory_of ctxt;

--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:10:19 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:43:29 2014 +0100
@@ -63,7 +63,7 @@
   
 val quickcheck_generator_cmd =
   gen_quickcheck_generator
-    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false})
+    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
     Syntax.read_term
   
 val _ =

--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:10:19 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:43:29 2014 +0100
@@ -71,7 +71,7 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding mapQ3}
-    ((Args.type_name {proper = false, strict = true} --| Scan.lift @{keyword "="}) --
+    ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
       (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
         Attrib.thm --| Scan.lift @{keyword ")"}) >>
       (fn (tyname, (relname, qthm)) =>

--- 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);