# HG changeset patch
# User wenzelm
# Date 1267132003 -3600
# Node ID df2b2168e43a6d8d09c95b41aa5e2cdaa5ddf392
# Parent  3ec03a3cd9d09b1814484d8348194e40bb00ae38
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;

diff -r 3ec03a3cd9d0 -r df2b2168e43a src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -182,7 +182,7 @@
      (Scan.succeed false);
 
 fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.tyname >>
+  (Args.goal_spec -- Args.type_name true >>
     (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
 fun setup_fresh_fun_simp x =
diff -r 3ec03a3cd9d0 -r df2b2168e43a src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -236,7 +236,7 @@
 
 (** document antiquotation **)
 
-val _ = ThyOutput.antiquotation "datatype" Args.tyname
+val _ = ThyOutput.antiquotation "datatype" (Args.type_name true)
   (fn {source = src, context = ctxt, ...} => fn dtco =>
     let
       val thy = ProofContext.theory_of ctxt;
diff -r 3ec03a3cd9d0 -r df2b2168e43a src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/Pure/Isar/args.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -54,7 +54,7 @@
   val term: term context_parser
   val term_abbrev: term context_parser
   val prop: term context_parser
-  val tyname: string context_parser
+  val type_name: bool -> string context_parser
   val const: string context_parser
   val const_proper: string context_parser
   val bang_facts: thm list context_parser
@@ -209,7 +209,8 @@
 
 (* type and constant names *)
 
-val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
+fun type_name strict =
+  Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
 val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
diff -r 3ec03a3cd9d0 -r df2b2168e43a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -52,7 +52,7 @@
   val infer_type: Proof.context -> string -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
-  val read_tyname: Proof.context -> string -> typ
+  val read_type_name: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> string -> term
   val read_const: Proof.context -> string -> term
   val allow_dummies: Proof.context -> Proof.context
@@ -414,7 +414,7 @@
 
 in
 
-fun read_tyname ctxt str =
+fun read_type_name ctxt strict str =
   let
     val thy = theory_of ctxt;
     val (c, pos) = token_content str;
@@ -425,8 +425,15 @@
     else
       let
         val d = Sign.intern_type thy c;
+        val decl = Sign.the_type_decl thy d;
         val _ = Position.report (Markup.tycon d) pos;
-      in Type (d, replicate (Sign.arity_number thy d) dummyT) end
+        fun err () = error ("Bad type name: " ^ quote d);
+        val args =
+          (case decl of
+            Type.LogicalType n => n
+          | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
+          | Type.Nonterminal => if strict then err () else 0);
+      in Type (d, replicate args dummyT) end
   end;
 
 fun read_const_proper ctxt = prep_const_proper ctxt o token_content;
diff -r 3ec03a3cd9d0 -r df2b2168e43a src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/Tools/Code/code_eval.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -144,7 +144,7 @@
 
 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
 val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
-  (Args.tyname --| Scan.lift (Args.$$$ "=")
+  (Args.type_name true --| Scan.lift (Args.$$$ "=")
     -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
       >> ml_code_datatype_antiq);
 
diff -r 3ec03a3cd9d0 -r df2b2168e43a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Feb 25 22:05:34 2010 +0100
+++ b/src/Tools/induct.ML	Thu Feb 25 22:06:43 2010 +0100
@@ -345,7 +345,7 @@
   Scan.lift (Args.$$$ k) >> K "";
 
 fun attrib add_type add_pred del =
-  spec typeN Args.tyname >> add_type ||
+  spec typeN (Args.type_name true) >> add_type ||
   spec predN Args.const >> add_pred ||
   spec setN Args.const >> add_pred ||
   Scan.lift Args.del >> K del;
@@ -856,7 +856,7 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule typeN Args.tyname get_type ||
+  named_rule typeN (Args.type_name true) get_type ||
   named_rule predN Args.const get_pred ||
   named_rule setN Args.const get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;