# HG changeset patch
# User paulson
# Date 1519563307 0
# Node ID b342f96e47b5380ddc8a0fc1d5e338c9392828e9
# Parent  17874d43d3b3d0b4fbbd14fca0818ab88031373f# Parent  bffb7482faaa0a94e87f77a594fb26e8db1b4e33
merged

diff -r bffb7482faaa -r b342f96e47b5 NEWS
--- a/NEWS	Sun Feb 25 12:54:55 2018 +0000
+++ b/NEWS	Sun Feb 25 12:55:07 2018 +0000
@@ -176,6 +176,12 @@
 (e.g. use 'find_theorems' or 'try' to figure this out).
 
 
+*** Pure ***
+
+* The inner syntax category "sort" now includes notation "_" for the
+dummy sort: it is effectively ignored in type-inference.
+
+
 *** HOL ***
 
 * Clarifed theorem names:
diff -r bffb7482faaa -r b342f96e47b5 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Feb 25 12:54:55 2018 +0000
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Feb 25 12:55:07 2018 +0000
@@ -724,7 +724,7 @@
     & \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
   @{syntax_def (inner) type_name} & = & \<open>id  |  longid\<close> \\\\
 
-  @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
+  @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
     & \<open>|\<close> & \<^verbatim>\<open>{\<close> @{syntax class_name} \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> @{syntax class_name} \<^verbatim>\<open>}\<close> \\
   @{syntax_def (inner) class_name} & = & \<open>id  |  longid\<close> \\
   \end{supertabular}
@@ -803,6 +803,9 @@
   \<^item> Dummy variables (written as underscore) may occur in different
   roles.
 
+    \<^descr> A sort ``\<open>_\<close>'' refers to a vacuous constraint for type variables, which
+    is effectively ignored in type-inference.
+
     \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
     parameter, which is filled-in according to the most general type produced
     by the type-checking phase.
diff -r bffb7482faaa -r b342f96e47b5 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Feb 25 12:54:55 2018 +0000
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Feb 25 12:55:07 2018 +0000
@@ -106,7 +106,8 @@
       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
       | classes _ = err ();
 
-    fun sort (Const ("_topsort", _)) = []
+    fun sort (Const ("_dummy_sort", _)) = dummyS
+      | sort (Const ("_topsort", _)) = []
       | sort (Const ("_sort", _) $ cs) = classes cs
       | sort (Const (s, _)) = [class s]
       | sort _ = err ();
@@ -506,10 +507,12 @@
     fun classes [c] = class c
       | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
   in
-    (case S of
-      [] => Syntax.const "_topsort"
-    | [c] => class c
-    | cs => Syntax.const "_sort" $ classes cs)
+    if S = dummyS then Syntax.const "_dummy_sort"
+    else
+      (case S of
+        [] => Syntax.const "_topsort"
+      | [c] => class c
+      | cs => Syntax.const "_sort" $ classes cs)
   end;
 
 
diff -r bffb7482faaa -r b342f96e47b5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Feb 25 12:54:55 2018 +0000
+++ b/src/Pure/pure_thy.ML	Sun Feb 25 12:55:07 2018 +0000
@@ -105,6 +105,7 @@
     ("",            typ "class_name => sort",          Mixfix.mixfix "_"),
     ("_class_name", typ "id => class_name",            Mixfix.mixfix "_"),
     ("_class_name", typ "longid => class_name",        Mixfix.mixfix "_"),
+    ("_dummy_sort", typ "sort",                        Mixfix.mixfix "'_"),
     ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
     ("_sort",       typ "classes => sort",             Mixfix.mixfix "{_}"),
     ("",            typ "class_name => classes",       Mixfix.mixfix "_"),