--- a/src/ZF/Tools/primrec_package.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Sep 15 17:16:56 2005 +0200
@@ -56,7 +56,7 @@
else strip_comb (hd middle);
val (cname, _) = dest_Const constr
handle TERM _ => raise RecError "ill-formed constructor";
- val con_info = the (Symtab.curried_lookup (ConstructorsData.get thy) cname)
+ val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
handle Option =>
raise RecError "cannot determine datatype associated with function"