# HG changeset patch
# User wenzelm
# Date 1121362109 -7200
# Node ID bbebc68a7fafbeaca1a9dd6dd67fb734037da25e
# Parent  bedf7b5fb78196a88363cabac881dd926101a2b0
occs no longer infix (structure not open);

diff -r bedf7b5fb781 -r bbebc68a7faf src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jul 14 19:28:28 2005 +0200
+++ b/src/Pure/logic.ML	Thu Jul 14 19:28:29 2005 +0200
@@ -6,8 +6,6 @@
 Abstract syntax operations of the Pure meta-logic.
 *)
 
-infix occs;
-
 signature LOGIC =
 sig
   val is_all            : term -> bool
@@ -179,7 +177,7 @@
 
 (*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 =