# HG changeset patch
# User wenzelm
# Date 1163197323 -3600
# Node ID 3c245a8a500138f8613e07aef536368ab2a7ac06
# Parent  63552bc99cfb6c6300345e9272cf72009609c874
avoid strange typing problem in MosML;

diff -r 63552bc99cfb -r 3c245a8a5001 src/Provers/IsaPlanner/zipper.ML
--- 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;