# HG changeset patch
# User wenzelm
# Date 1379365682 -7200
# Node ID bcfd16f65014fb15dfa537e4dd0a8e5fd784311b
# Parent  df8068269e90d513e9d681bc07c122f40e558755
treat all dummy type variables separately (in contrast to fca432074fb2);

diff -r df8068269e90 -r bcfd16f65014 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 16 23:04:13 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 16 23:08:02 2013 +0200
@@ -626,9 +626,11 @@
     val tsig = tsig_of ctxt;
     val defaultS = Type.defaultS tsig;
 
+    val dummy_var = ("'_dummy_", ~1);
+
     fun constraint (xi, raw_S) env =
       let val (ps, S) = Term_Position.decode_positionS raw_S in
-        if S = dummyS then env
+        if xi = dummy_var orelse S = dummyS then env
         else
           Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
             handle Vartab.DUP _ =>
@@ -642,17 +644,20 @@
           | TVar v => constraint v
           | _ => I) tys Vartab.empty;
 
-    fun get_sort xi =
-      (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
-        (NONE, NONE) => defaultS
-      | (NONE, SOME S) => S
-      | (SOME S, NONE) => S
-      | (SOME S, SOME S') =>
-          if Type.eq_sort tsig (S, S') then S'
-          else
-            error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
-              " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
-              " for type variable " ^ quote (Term.string_of_vname' xi)));
+    fun get_sort xi raw_S =
+      if xi = dummy_var then
+        Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S))
+      else
+        (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
+          (NONE, NONE) => defaultS
+        | (NONE, SOME S) => S
+        | (SOME S, NONE) => S
+        | (SOME S, SOME S') =>
+            if Type.eq_sort tsig (S, S') then S'
+            else
+              error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
+                " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
+                " for type variable " ^ quote (Term.string_of_vname' xi)));
 
     fun add_report S pos reports =
       if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
@@ -662,7 +667,7 @@
     fun get_sort_reports xi raw_S =
       let
         val ps = #1 (Term_Position.decode_positionS raw_S);
-        val S = get_sort xi handle ERROR msg => error (msg ^ Position.here_list ps);
+        val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps);
       in fold (add_report S) ps end;
 
     val reports =
@@ -683,8 +688,8 @@
       if Term_Position.is_positionT T then T
       else
         (case T of
-          TFree (x, _) => TFree (x, get_sort (x, ~1))
-        | TVar (xi, _) => TVar (xi, get_sort xi)
+          TFree (x, raw_S) => TFree (x, get_sort (x, ~1) raw_S)
+        | TVar (xi, raw_S) => TVar (xi, get_sort xi raw_S)
         | _ => T));
 
 in