--- a/src/Provers/IsaPlanner/zipper.ML Fri Nov 10 23:22:01 2006 +0100
+++ b/src/Provers/IsaPlanner/zipper.ML Fri Nov 10 23:22:03 2006 +0100
@@ -21,10 +21,10 @@
type cname (* constant names *)
type vname (* meta variable names *)
type bname (* bound var name *)
-datatype term = Const of (cname * typ)
- | Abs of (aname * typ * term)
- | Free of (fname * typ)
- | Var of (vname * typ)
+datatype term = Const of cname * typ
+ | Abs of aname * typ * term
+ | Free of fname * typ
+ | Var of vname * typ
| Bound of bname
| $ of term * term;
type T = term;