--- 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 *****)