src/HOLCF/fixrec_package.ML
changeset 20155 da0505518e69
parent 20071 8f3e1ddb50e6
child 20854 f9cf9e62d11c
--- a/src/HOLCF/fixrec_package.ML	Wed Jul 19 12:11:56 2006 +0200
+++ b/src/HOLCF/fixrec_package.ML	Wed Jul 19 12:11:57 2006 +0200
@@ -57,7 +57,7 @@
 (* infers the type of a term *)  (* FIXME better avoid this low-level stuff *)
 (* similar to Theory.inferT_axm, but allows any type, not just propT *)
 fun infer sg t =
-  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true
+  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true
     ([t],dummyT));
 
 (* builds the expression (LAM v. rhs) *)