diff -r 04502e5431fb -r 9112a2efb9a3 TFL/tfl.sml
--- a/TFL/tfl.sml	Tue May 27 13:03:41 1997 +0200
+++ b/TFL/tfl.sml	Tue May 27 13:22:30 1997 +0200
@@ -8,9 +8,7 @@
 
 functor TFL(structure Rules : Rules_sig
             structure Thry  : Thry_sig
-            structure Thms  : Thms_sig
-            sharing type Rules.binding = Thry.binding = 
-                         Thry.USyntax.binding = Mask.binding) : TFL_sig  =
+            structure Thms  : Thms_sig) : TFL_sig  =
 struct
 
 (* Declarations *)
@@ -25,14 +23,10 @@
 structure S = USyntax;
 structure U = S.Utils;
 
-(* Declares 'a binding datatype *)
-open Mask;
-
-nonfix mem --> |->;
+nonfix mem -->;
 val --> = S.-->;
 
 infixr 3 -->;
-infixr 7 |->;
 
 val concl = #2 o R.dest_thm;
 val hyp = #1 o R.dest_thm;
@@ -118,8 +112,8 @@
 datatype pattern = GIVEN   of term * int
                  | OMITTED of term * int
 
-fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
-  | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
+fun psubst theta (GIVEN (tm,i)) = GIVEN(subst_free theta tm, i)
+  | psubst theta (OMITTED (tm,i)) = OMITTED(subst_free theta tm, i);
 
 fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
   | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
@@ -217,7 +211,7 @@
        then let val fresh = fresh_constr ty_match ty fresh_var
                 fun expnd (c,gvs) = 
                   let val capp = list_comb(c,gvs)
-                  in ((prefix, capp::rst), psubst[p |-> capp] rhs)
+                  in ((prefix, capp::rst), psubst[(p,capp)] rhs)
                   end
             in map expnd (map fresh constructors)  end
        else [row]
@@ -235,7 +229,7 @@
          val col0 = map(hd o #2) pat_rectangle
      in 
      if (forall is_Free col0) 
-     then let val rights' = map (fn(v,e) => psubst[v|->u] e)
+     then let val rights' = map (fn(v,e) => psubst[(v,u)] e)
                                 (ListPair.zip (col0, rights))
               val pat_rectangle' = map v_to_prefix pat_rectangle
               val (pref_patl,tm) = mk{path = rstp,
@@ -330,7 +324,7 @@
              of [] => ()
           | L => mk_functional_err("The following rows (counting from zero)\
                                    \ are inaccessible: "^stringize L)
-     val case_tm' = S.subst [f |-> fvar] case_tm
+     val case_tm' = subst_free [(f,fvar)] case_tm
  in {functional = S.list_mk_abs ([fvar,a], case_tm'),
      pats = patts2}
 end end;
@@ -497,7 +491,7 @@
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
      val (def,theory) = Thry.make_definition thy (Name ^ "_def") 
-                                                 (S.subst[R1 |-> R'] proto_def)
+                                               (subst_free[(R1,R')] proto_def)
      val fconst = #lhs(S.dest_eq(concl def)) 
      val tych = Thry.typecheck theory
      val baz = R.DISCH (tych proto_def)
@@ -571,7 +565,7 @@
  let 
  val divide = ipartition (gvvariant FV)
  val tych = Thry.typecheck thy
- fun tych_binding(x|->y) = (tych x |-> tych y)
+ fun tych_binding(x,y) = (tych x, tych y)
  fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
  fun mk{rows=[],...} = fail"no rows"
    | mk{path=[], rows = [([], (thm, bindings))]} = 
@@ -582,7 +576,7 @@
          val pat_rectangle' = map tl pat_rectangle
      in 
      if (forall is_Free col0) (* column 0 is all variables *)
-     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
+     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
                                 (ListPair.zip (rights, col0))
           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
           end