# HG changeset patch
# User wenzelm
# Date 1312921833 -7200
# Node ID 202d2f56560c71e38eb117424ec1010238f3c7a8
# Parent  2cf62c4e6c7a50b4fcffd398af07e7b93073a843
misc tuning and clarification;

diff -r 2cf62c4e6c7a -r 202d2f56560c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 09 21:48:36 2011 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 09 22:30:33 2011 +0200
@@ -567,13 +567,16 @@
 
 (**** Freezing and thawing of variables in proof terms ****)
 
+local
+
 fun frzT names =
-  map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs));
+  map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S));
 
 fun thawT names =
-  map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of
-      NONE => TFree (s, xs)
-    | SOME ixn => TVar (ixn, xs));
+  map_type_tfree (fn (a, S) =>
+    (case AList.lookup (op =) names a of
+      NONE => TFree (a, S)
+    | SOME ixn => TVar (ixn, S)));
 
 fun freeze names names' (t $ u) =
       freeze names names' t $ freeze names names' u
@@ -582,7 +585,7 @@
   | 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 ((the o AList.lookup (op =) names) ixn, frzT names' T)
+      Free (the (AList.lookup (op =) names ixn), frzT names' T)
   | freeze names names' t = t;
 
 fun thaw names names' (t $ u) =
@@ -591,14 +594,16 @@
       Abs (s, thawT names' T, thaw names names' t)
   | thaw names names' (Const (s, T)) = Const (s, thawT names' T)
   | thaw names names' (Free (s, T)) =
-      let val T' = thawT names' T
-      in case AList.lookup (op =) names s of
+      let val T' = thawT names' T in
+        (case AList.lookup (op =) names s of
           NONE => Free (s, T')
-        | SOME ixn => Var (ixn, T')
+        | SOME ixn => Var (ixn, T'))
       end
   | thaw names names' (Var (ixn, T)) = Var (ixn, thawT names' T)
   | thaw names names' t = t;
 
+in
+
 fun freeze_thaw_prf prf =
   let
     val (fs, Tfs, vs, Tvs) = fold_proof_terms
@@ -618,6 +623,8 @@
      map_proof_terms (thaw rnames rnames') (thawT rnames'))
   end;
 
+end;
+
 
 (***** implication introduction *****)