# HG changeset patch
# User wenzelm
# Date 1006986659 -3600
# Node ID fed7bed97293f3989b8e8247fe1aaa60e79bc49f
# Parent  79138d75405fbdb1bf36c24460c937df2c8fdb7f
support "_::foo" sort constraints;

diff -r 79138d75405f -r fed7bed97293 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Nov 28 23:30:24 2001 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Nov 28 23:30:59 2001 +0100
@@ -10,7 +10,7 @@
 sig
   val sort_of_term: term -> sort
   val raw_term_sorts: term -> (indexname * sort) list
-  val typ_of_term: (indexname -> sort) -> term -> typ
+  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
 end;
@@ -62,16 +62,15 @@
 
 (* typ_of_term *)
 
-fun typ_of_term get_sort t =
+fun typ_of_term get_sort map_sort t =
   let
     fun typ_of (Free (x, _)) =
           if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
           else Type (x, [])
       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
-      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) =
-          TFree (x, get_sort (x, ~1))
-      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) =
-          TVar (xi, get_sort xi)
+      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
+      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
+      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", map_sort (sort_of_term t))
       | typ_of tm =
           let
             val (t, ts) = strip_comb tm;
@@ -80,9 +79,7 @@
                 Const (x, _) => x
               | Free (x, _) => x
               | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
-          in
-            Type (a, map typ_of ts)
-          end;
+          in Type (a, map typ_of ts) end;
   in typ_of t end;
 
 
@@ -186,6 +183,7 @@
    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
+   Mfix ("'_::_",       sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
    Mfix ("_",           longidT --> sortT,             "", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),