# HG changeset patch
# User wenzelm
# Date 1139338618 -3600
# Node ID 593af1a1068bd9c2e8977636f200dbf9f09d1ac5
# Parent  f88976608aad249ac3904521a3fb7df126ca4e27
adapted Sign.infer_types;
removed obsolete lambda' -- same as Term.lambda;

diff -r f88976608aad -r 593af1a1068b src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Tue Feb 07 19:56:57 2006 +0100
+++ b/src/HOLCF/fixrec_package.ML	Tue Feb 07 19:56:58 2006 +0100
@@ -50,19 +50,14 @@
 infix 1 ===; fun S === T = %%:"op =" $ S $ T;
 infix 9 `  ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x;
 
-(* infers the type of a term *)
+(* 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 (K NONE) (K NONE) [] true ([t],dummyT));
-
-(* Similar to Term.lambda, but also allows abstraction over constants *)
-fun lambda' (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
-  | lambda' (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
-  | lambda' (v as Const (x, T)) t = Abs (Sign.base_name x, T, abstract_over (v, t))
-  | lambda' v t = raise TERM ("lambda'", [v, t]);
+  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true
+    ([t],dummyT));
 
 (* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(lambda' v rhs);
+fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs);
 
 (* builds the expression (LAM v1 v2 .. vn. rhs) *)
 fun big_lambdas [] rhs = rhs