src/Pure/term.ML
changeset 40 3f9f8395519e
parent 0 a5a9c433f639
child 61 f8c1922b78e3
equal deleted inserted replaced
39:deb04a336a99 40:3f9f8395519e
    50 
    50 
    51 
    51 
    52 (*For errors involving type mismatches*)
    52 (*For errors involving type mismatches*)
    53 exception TYPE of string * typ list * term list;
    53 exception TYPE of string * typ list * term list;
    54 
    54 
       
    55 fun raise_type msg tys ts = raise TYPE (msg, tys, ts);
       
    56 
    55 (*For system errors involving terms*)
    57 (*For system errors involving terms*)
    56 exception TERM of string * term list;
    58 exception TERM of string * term list;
       
    59 
       
    60 fun raise_term msg ts = raise TERM (msg, ts);
    57 
    61 
    58 
    62 
    59 (*Note variable naming conventions!
    63 (*Note variable naming conventions!
    60     a,b,c: string
    64     a,b,c: string
    61     f,g,h: functions (including terms of function type)
    65     f,g,h: functions (including terms of function type)