src/Pure/proofterm.ML

 
 
 (**** Freezing and thawing of variables in proof terms ****)
 
 fun frzT names =
-  map_type_tvar (fn (ixn, xs) => TFree (valOf (assoc (names, ixn)), xs));
+  map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs));
 
 fun thawT names =
   map_type_tfree (fn (s, xs) => case assoc (names, s) of
       NONE => TFree (s, xs)
     | SOME ixn => TVar (ixn, xs));

   | freeze names names' (Abs (s, T, t)) =
       Abs (s, frzT names' T, freeze names names' t)
   | freeze names names' (Const (s, T)) = Const (s, frzT names' T)
   | freeze names names' (Free (s, T)) = Free (s, frzT names' T)
   | freeze names names' (Var (ixn, T)) =
-      Free (valOf (assoc (names, ixn)), frzT names' T)
+      Free (the (assoc (names, ixn)), frzT names' T)
   | freeze names names' t = t;
 
 fun thaw names names' (t $ u) =
       thaw names names' t $ thaw names names' u
   | thaw names names' (Abs (s, T, t)) =

   let
     val fs = add_term_tfrees (t, []) \\ fixed;
     val ixns = add_term_tvar_ixns (t, []);
     val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
     fun thaw (f as (a, S)) =
-      (case gen_assoc (op =) (fmap, f) of
+      (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME b => TVar ((b, 0), S));
   in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
   end;
 

       add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
   | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
   | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
 and add_npvars' Ts (vs, t) = (case strip_comb t of
     (Var (ixn, _), ts) => if test_args [] ts then vs
-      else Library.foldl (add_npvars' Ts) (overwrite (vs,
-        (ixn, Library.foldl (add_funvars Ts) (getOpt (assoc (vs, ixn), []), ts))), ts)
+      else Library.foldl (add_npvars' Ts)
+        (AList.update (op =) (ixn,
+          Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts)
   | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
 
 fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
   | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t