src/Pure/logic.ML

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
 
 Abstract syntax operations of the Pure meta-logic.
 *)
-
-infix occs;
 
 signature LOGIC =
 sig
   val is_all            : term -> bool
   val mk_equals         : term * term -> term

 
 (*** Low-level term operations ***)
 
 (*Does t occur in u?  Or is alpha-convertible to u?
   The term t must contain no loose bound variables*)
-fun t occs u = exists_subterm (fn s => t aconv s) u;
+fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
 
 (*Close up a formula over all free variables by quantification*)
 fun close_form A =
   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);