files now define a structure to allow SML/NJ to optimize the code

--- a/src/Pure/library.ML	Wed Nov 22 18:48:56 1995 +0100
+++ b/src/Pure/library.ML	Thu Nov 23 12:18:16 1995 +0100
@@ -8,6 +8,11 @@
 input / output, timing, filenames, misc functions.
 *)
 
+infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset;
+
+
+structure Library =
+struct
 
 (** functions **)
 
@@ -18,11 +23,9 @@
 fun K x y = x;
 
 (*reverse apply*)
-infix |>;
 fun (x |> f) = f x;
 
 (*combine two functions forming the union of their domains*)
-infix orelf;
 fun f orelf g = fn x => f x handle Match => g x;
 
 (*application of (infix) operator to its left or right argument*)
@@ -92,10 +95,8 @@
 
 (* operators for combining predicates *)
 
-infix orf;
 fun p orf q = fn x => p x orelse q x;
 
-infix andf;
 fun p andf q = fn x => p x andalso q x;
 
 fun notf p x = not (p x);
@@ -272,7 +273,6 @@
 
 (*combine two lists forming a list of pairs:
   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
-infix ~~;
 fun [] ~~ [] = []
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   | _ ~~ _ = raise LIST "~~";
@@ -285,7 +285,6 @@
 
 (* prefixes, suffixes *)
 
-infix prefix;
 fun [] prefix _ = true
   | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys)
   | _ prefix _ = false;
@@ -317,12 +316,10 @@
 (* lists of integers *)
 
 (*make the list [from, from + 1, ..., to]*)
-infix upto;
 fun from upto to =
   if from > to then [] else from :: ((from + 1) upto to);
 
 (*make the list [from, from - 1, ..., to]*)
-infix downto;
 fun from downto to =
   if from < to then [] else from :: ((from - 1) downto to);
 
@@ -429,7 +426,6 @@
 (** lists as sets **)
 
 (*membership in a list*)
-infix mem;
 fun x mem [] = false
   | x mem (y :: ys) = x = y orelse x mem ys;
 
@@ -439,7 +435,6 @@
 
 
 (*insertion into list if not already there*)
-infix ins;
 fun x ins xs = if x mem xs then xs else x :: xs;
 
 (*generalized insertion*)
@@ -447,7 +442,6 @@
 
 
 (*union of sets represented as lists: no repetitions*)
-infix union;
 fun xs union [] = xs
   | [] union ys = ys
   | (x :: xs) union ys = xs union (x ins ys);
@@ -459,14 +453,12 @@
 
 
 (*intersection*)
-infix inter;
 fun [] inter ys = []
   | (x :: xs) inter ys =
       if x mem ys then x :: (xs inter ys) else xs inter ys;
 
 
 (*subset*)
-infix subset;
 fun [] subset ys = true
   | (x :: xs) subset ys = x mem ys andalso xs subset ys;
 
@@ -480,11 +472,9 @@
 
 
 (*removing an element from a list WITHOUT duplicates*)
-infix \;
 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   | [] \ x = [];
 
-infix \\;
 val op \\ = foldl (op \);
 
 (*removing an element from a list -- possibly WITH duplicates*)
@@ -860,3 +850,6 @@
             in implode lets :: scanwords is_let rest end;
   in scan1 (#2 (take_prefix (not o is_let) cs)) end;
 
+end;
+
+open Library;

--- a/src/Pure/term.ML	Wed Nov 22 18:48:56 1995 +0100
+++ b/src/Pure/term.ML	Thu Nov 23 12:18:16 1995 +0100
@@ -2,11 +2,18 @@
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
+
+Simply typed lambda-calculus: types, terms, and basic operations
 *)
 
+infix 9  $;
+infixr 5 -->;
+infixr   --->;
+infix    aconv;
+
 
-(*Simply typed lambda-calculus: types, terms, and basic operations*)
-
+structure Term =
+struct
 
 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   for resolution.*)
@@ -21,11 +28,9 @@
              | TFree of string * sort
 	     | TVar  of indexname * sort;
 
-infixr 5 -->;
 fun S --> T = Type("fun",[S,T]);
 
 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
-infixr --->;
 val op ---> = foldr (op -->);
 
 
@@ -39,7 +44,6 @@
 
 
 
-infix 9 $;  (*application binds tightly!*)
 datatype term = 
     Const of string * typ
   | Free  of string * typ 
@@ -304,7 +308,6 @@
 
 (*Tests whether 2 terms are alpha-convertible and have same type.
   Note that constants and Vars may have more than one type.*)
-infix aconv;
 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   | (Free(a,T)) aconv (Free(b,U)) = a=b  andalso  T=U
   | (Var(v,T)) aconv (Var(w,U)) =   v=w  andalso  T=U
@@ -588,3 +591,7 @@
   in foldl rename_aT ([],vars) end;
 
 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
+
+end;
+
+open Term;