# HG changeset patch
# User wenzelm
# Date 1214257548 -7200
# Node ID e8eef124d0fd3dc299e8777edaf6dde2ace42bd7
# Parent  3f17273766f2e9d2c4b716980c61053e34996aa7
moved implies to logic.ML;
removed equals;
qualified all;

diff -r 3f17273766f2 -r e8eef124d0fd src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Jun 23 23:45:47 2008 +0200
+++ b/src/Pure/term.ML	Mon Jun 23 23:45:48 2008 +0200
@@ -82,9 +82,6 @@
   structure Typtab: TABLE
   structure Termtab: TABLE
   val propT: typ
-  val implies: term
-  val all: typ -> term
-  val equals: typ -> term
   val strip_all_body: term -> term
   val strip_all_vars: term -> (string * typ) list
   val incr_bv: int * int * term -> term
@@ -152,6 +149,7 @@
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
+  val all: typ -> term
   val argument_type_of: term -> int -> typ
   val head_name_of: term -> string
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
@@ -726,12 +724,8 @@
 
 val propT : typ = Type("prop",[]);
 
-val implies = Const("==>", propT-->propT-->propT);
-
 fun all T = Const("all", (T-->propT)-->propT);
 
-fun equals T = Const("==", T-->T-->propT);
-
 (* maps  !!x1...xn. t   to   t  *)
 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   | strip_all_body t  =  t;
@@ -1204,8 +1198,7 @@
       | name_clash (Abs (_, _, t)) = name_clash t
       | name_clash _ = false;
   in
-    if name_clash body then
-      dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
+    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
     else (x, subst_bound (Free (x, T), body))
   end;