src/Pure/term.ML
changeset 27335 e8eef124d0fd
parent 25050 0dc445970b4b
child 29256 2f1759641087
     1.1 --- a/src/Pure/term.ML	Mon Jun 23 23:45:47 2008 +0200
     1.2 +++ b/src/Pure/term.ML	Mon Jun 23 23:45:48 2008 +0200
     1.3 @@ -82,9 +82,6 @@
     1.4    structure Typtab: TABLE
     1.5    structure Termtab: TABLE
     1.6    val propT: typ
     1.7 -  val implies: term
     1.8 -  val all: typ -> term
     1.9 -  val equals: typ -> term
    1.10    val strip_all_body: term -> term
    1.11    val strip_all_vars: term -> (string * typ) list
    1.12    val incr_bv: int * int * term -> term
    1.13 @@ -152,6 +149,7 @@
    1.14    val aT: sort -> typ
    1.15    val itselfT: typ -> typ
    1.16    val a_itselfT: typ
    1.17 +  val all: typ -> term
    1.18    val argument_type_of: term -> int -> typ
    1.19    val head_name_of: term -> string
    1.20    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.21 @@ -726,12 +724,8 @@
    1.22  
    1.23  val propT : typ = Type("prop",[]);
    1.24  
    1.25 -val implies = Const("==>", propT-->propT-->propT);
    1.26 -
    1.27  fun all T = Const("all", (T-->propT)-->propT);
    1.28  
    1.29 -fun equals T = Const("==", T-->T-->propT);
    1.30 -
    1.31  (* maps  !!x1...xn. t   to   t  *)
    1.32  fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
    1.33    | strip_all_body t  =  t;
    1.34 @@ -1204,8 +1198,7 @@
    1.35        | name_clash (Abs (_, _, t)) = name_clash t
    1.36        | name_clash _ = false;
    1.37    in
    1.38 -    if name_clash body then
    1.39 -      dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
    1.40 +    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
    1.41      else (x, subst_bound (Free (x, T), body))
    1.42    end;
    1.43