Changed function cabs to also allow abstraction over Vars.
authorberghofe
Tue Oct 26 16:34:19 2004 +0200 (2004-10-26)
changeset 15264a881ad2e9edc
parent 15263 b40e91201039
child 15265 a1547232fedd
Changed function cabs to also allow abstraction over Vars.
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Oct 26 16:33:35 2004 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Oct 26 16:34:19 2004 +0200
     1.3 @@ -226,11 +226,11 @@
     1.4        else raise CTERM "capply: types don't agree"
     1.5    | capply _ _ = raise CTERM "capply: first arg is not a function"
     1.6  
     1.7 -fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
     1.8 +fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
     1.9           (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
    1.10 -      Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
    1.11 -             T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
    1.12 -  | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
    1.13 +      Cterm {t=Sign.nodup_vars (lambda t1 t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
    1.14 +             T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
    1.15 +      handle TERM _ => raise CTERM "cabs: first arg is not a variable";
    1.16  
    1.17  (*Matching of cterms*)
    1.18  fun gen_cterm_match mtch