src/Pure/Syntax/syn_ext.ML
changeset 28856 5e009a80fe6d
parent 26704 51ee753cc2e3
child 28904 3ef9489eeef5
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val dddot_indexname: indexname
     1.5    val constrainC: string
     1.6    val typeT: typ
     1.7 +  val spropT: typ
     1.8    val max_pri: int
     1.9    val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
    1.10    val mk_trfun: string * 'a -> string * ('a * stamp)