1.1 --- a/src/Pure/pure_thy.ML	Thu Oct 16 22:44:30 2008 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Oct 16 22:44:31 2008 +0200
     1.3 @@ -309,7 +309,8 @@
     1.4      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     1.5      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     1.6      ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
     1.7 -    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_")]
     1.8 +    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
     1.9 +    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))")]
    1.10    #> Sign.add_syntax_i applC_syntax
    1.11    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    1.12     [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    1.13 @@ -349,13 +350,18 @@
    1.14    #> Sign.local_path
    1.15    #> Sign.add_consts_i
    1.16     [("term", typ "'a => prop", NoSyn),
    1.17 +    ("sort_constraint", typ "'a itself => prop", NoSyn),
    1.18      ("conjunction", typ "prop => prop => prop", NoSyn)]
    1.19    #> (add_defs false o map Thm.no_attributes)
    1.20     [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
    1.21      ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
    1.22 +    ("sort_constraint_def",
    1.23 +      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
    1.24 +      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
    1.25      ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
    1.26 +  #> Sign.hide_const false "Pure.term"
    1.27 +  #> Sign.hide_const false "Pure.sort_constraint"
    1.28    #> Sign.hide_const false "Pure.conjunction"
    1.29 -  #> Sign.hide_const false "Pure.term"
    1.30    #> add_thmss [(("nothing", []), [])] #> snd
    1.31    #> Theory.add_axioms_i Proofterm.equality_axms));
    1.32