# HG changeset patch
# User wenzelm
# Date 1330103646 -3600
# Node ID bb185c45037e52192b01f0d7d70bf0df726712d1
# Parent  689ebcbd634392a4a2b48d713521a5d0011bede1
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;

diff -r 689ebcbd6343 -r bb185c45037e src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Feb 24 18:14:06 2012 +0100
@@ -27,7 +27,7 @@
   val fbreakN: string val fbreak: Markup.T
   val hiddenN: string val hidden: Markup.T
   val classN: string
-  val typeN: string
+  val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> Markup.T
   val dynamic_factN: string val dynamic_fact: string -> Markup.T
@@ -174,7 +174,7 @@
 (* logical entities *)
 
 val classN = "class";
-val typeN = "type";
+val type_nameN = "type name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
diff -r 689ebcbd6343 -r bb185c45037e src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Feb 24 18:14:06 2012 +0100
@@ -78,7 +78,7 @@
   /* logical entities */
 
   val CLASS = "class"
-  val TYPE = "type"
+  val TYPE_NAME = "type name"
   val FIXED = "fixed"
   val CONSTANT = "constant"
 
diff -r 689ebcbd6343 -r bb185c45037e src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/type.ML	Fri Feb 24 18:14:06 2012 +0100
@@ -187,7 +187,7 @@
 
 val empty_tsig =
   build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
-    Name_Space.empty_table Isabelle_Markup.typeN);
+    Name_Space.empty_table Isabelle_Markup.type_nameN);
 
 
 (* classes and sorts *)