changeset 39288 | f1ae2493d93f |
parent 37781 | 2fbbf0a48cef |
child 39557 | fe5722fce758 |
--- 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;