changeset 14820 | 3f80d6510ee9 |
parent 14240 | d3843feb9de7 |
child 15531 | 08c8dad8e399 |
--- a/TFL/tfl.ML Sat May 29 14:58:44 2004 +0200 +++ b/TFL/tfl.ML Sat May 29 14:59:24 2004 +0200 @@ -371,7 +371,7 @@ (*For Isabelle, the lhs of a definition must be a constant.*) fun mk_const_def sign (Name, Ty, rhs) = - Sign.infer_types sign (K None) (K None) [] false + Sign.infer_types (Sign.pp sign) sign (K None) (K None) [] false ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT) |> #1;