# HG changeset patch
# User wenzelm
# Date 1224189871 -7200
# Node ID 1a0b845855aca3cb00cccceb2400768eb63e7902
# Parent  a60164e8fff0418c59be090f1c43e4f864338b2c
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;

diff -r a60164e8fff0 -r 1a0b845855ac src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Oct 16 22:44:30 2008 +0200
+++ b/src/Pure/pure_thy.ML	Thu Oct 16 22:44:31 2008 +0200
@@ -309,7 +309,8 @@
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
-    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_")]
+    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
+    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))")]
   #> Sign.add_syntax_i applC_syntax
   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
@@ -349,13 +350,18 @@
   #> Sign.local_path
   #> Sign.add_consts_i
    [("term", typ "'a => prop", NoSyn),
+    ("sort_constraint", typ "'a itself => prop", NoSyn),
     ("conjunction", typ "prop => prop => prop", NoSyn)]
   #> (add_defs false o map Thm.no_attributes)
    [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
     ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+    ("sort_constraint_def",
+      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
+      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
     ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+  #> Sign.hide_const false "Pure.term"
+  #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
-  #> Sign.hide_const false "Pure.term"
   #> add_thmss [(("nothing", []), [])] #> snd
   #> Theory.add_axioms_i Proofterm.equality_axms));