tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);

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

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -33,7 +33,8 @@
       error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
 
     val fpT_names =
-      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
+      map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
+        raw_fpT_names;
 
     fun lfp_sugar_of s =
       (case fp_sugar_of lthy s of

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -234,7 +234,7 @@
 (** document antiquotation **)
 
 val antiq_setup =
-  Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
+  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, 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 11:32:16 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -61,8 +61,10 @@
 
 val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
   
-val quickcheck_generator_cmd = gen_quickcheck_generator
-  (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+val quickcheck_generator_cmd =
+  gen_quickcheck_generator
+    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false})
+    Syntax.read_term
   
 val _ =
   Outer_Syntax.command @{command_spec "quickcheck_generator"}

--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -71,7 +71,7 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding mapQ3}
-    ((Args.type_name true --| Scan.lift @{keyword "="}) --
+    ((Args.type_name {proper = false, 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/HOL/Tools/coinduction.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -129,7 +129,7 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule Induct.typeN (Args.type_name false) get_type ||
+  named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
   named_rule Induct.predN (Args.const false) get_pred ||
   named_rule Induct.setN (Args.const false) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;

--- a/src/Pure/Isar/args.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -56,7 +56,7 @@
   val term_pattern: term context_parser
   val term_abbrev: term context_parser
   val prop: term context_parser
-  val type_name: bool -> string context_parser
+  val type_name: {proper: bool, strict: bool} -> string context_parser
   val const: bool -> string context_parser
   val const_proper: bool -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
@@ -208,8 +208,8 @@
 
 (* type and constant names *)
 
-fun type_name strict =
-  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
+fun type_name flags =
+  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
 fun const strict =

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -68,12 +68,9 @@
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
-  val check_type_name: Proof.context -> bool ->
+  val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     xstring * Position.T -> typ * Position.report list
-  val check_type_name_proper: Proof.context -> bool ->
-    xstring * Position.T -> typ * Position.report list
-  val read_type_name: Proof.context -> bool -> string -> typ
-  val read_type_name_proper: Proof.context -> bool -> string -> typ
+  val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
   val check_const_proper: Proof.context -> bool ->
     xstring * Position.T -> term * Position.report list
   val read_const_proper: Proof.context -> bool -> string -> term
@@ -443,13 +440,15 @@
 
 (* type names *)
 
-fun check_type_name ctxt strict (c, pos) =
+fun check_type_name ctxt {proper, strict} (c, pos) =
   if Lexicon.is_tid c then
-    let
-      val reports =
-        if Context_Position.is_reported ctxt pos
-        then [(pos, Markup.tfree)] else [];
-    in (TFree (c, default_sort ctxt (c, ~1)), reports) end
+    if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
+    else
+      let
+        val reports =
+          if Context_Position.is_reported ctxt pos
+          then [(pos, Markup.tfree)] else [];
+      in (TFree (c, default_sort ctxt (c, ~1)), reports) end
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
@@ -461,16 +460,12 @@
         | Type.Nonterminal => if strict then err () else 0);
     in (Type (d, replicate args dummyT), reports) end;
 
-fun check_type_name_proper ctxt strict arg =
-  (case check_type_name ctxt strict arg of
-    res as (Type _, _) => res
-  | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
-
-fun read_type_name ctxt strict =
-  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1;
-
-fun read_type_name_proper ctxt strict =
-  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1;
+fun read_type_name ctxt flags text =
+  let
+    val (T, reports) =
+      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+    val _ = Position.reports reports;
+  in T end;
 
 
 (* constant names *)
@@ -531,7 +526,8 @@
 in
 
 val read_arity =
-  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+  prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
+    Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 

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

--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -127,7 +127,7 @@
 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
+      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
       val res =
         (case try check (c, decl) of

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -170,7 +170,8 @@
           let
             val pos = Lexicon.pos_of_token tok;
             val (Type (c, _), rs) =
-              Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
+              Proof_Context.check_type_name ctxt {proper = true, strict = false}
+                (Lexicon.str_of_token tok, pos);
             val _ = Unsynchronized.change reports (append (map (rpair "") rs));
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok

--- a/src/Pure/Thy/thy_output.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -515,7 +515,7 @@
   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
 
 fun pretty_type ctxt s =
-  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
+  let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;

--- a/src/Tools/Code/code_target.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -97,8 +97,8 @@
       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
-fun read_tyco ctxt = #1 o dest_Type
-  o Proof_Context.read_type_name_proper ctxt true;
+fun read_tyco ctxt =
+  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
 
 fun cert_class ctxt class =
   let

--- a/src/Tools/induct.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Tools/induct.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -361,7 +361,7 @@
   Scan.lift (Args.$$$ k) >> K "";
 
 fun attrib add_type add_pred del =
-  spec typeN (Args.type_name false) >> add_type ||
+  spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
   spec predN (Args.const false) >> add_pred ||
   spec setN (Args.const false) >> add_pred ||
   Scan.lift Args.del >> K del;
@@ -883,7 +883,7 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule typeN (Args.type_name false) get_type ||
+  named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
   named_rule predN (Args.const false) get_pred ||
   named_rule setN (Args.const false) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;