diff -r d30be6791038 -r f1ae2493d93f src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -403,7 +403,7 @@
   let
     val ctxt = ProofContext.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
+      map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;