--- a/src/Pure/logic.ML Tue Mar 08 16:02:52 2005 +0100
+++ b/src/Pure/logic.ML Wed Mar 09 18:44:52 2005 +0100
@@ -336,6 +336,7 @@
(*Inverse of varify. Converts axioms back to their original form.*)
fun unvarify (Const(a,T)) = Const(a, Type.unvarifyT T)
+ | unvarify (Free(a,T)) = Free(a, Type.unvarifyT T) (* CB: added *)
| unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
| unvarify (Var(ixn,T)) = Var(ixn, Type.unvarifyT T) (*non-0 index!*)
| unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)