TFL/tfl.ML

--- a/TFL/tfl.ML	Wed Jul 19 12:11:56 2006 +0200
+++ b/TFL/tfl.ML	Wed Jul 19 12:11:57 2006 +0200
@@ -367,7 +367,7 @@
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun mk_const_def sign (c, Ty, rhs) =
-    Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) [] false
+    Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false
                ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
     |> #1;