1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Aug 30 21:44:29 2007 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Aug 30 22:35:34 2007 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4  
     1.5  (*For Isabelle, the lhs of a definition must be a constant.*)
     1.6  fun mk_const_def sign (c, Ty, rhs) =
     1.7 -  singleton (ProofContext.infer_types (ProofContext.init sign))
     1.8 +  singleton (Syntax.check_terms (ProofContext.init sign))
     1.9      (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
    1.10  
    1.11  (*Make all TVars available for instantiation by adding a ? to the front*)