src/Pure/thm.ML
changeset 32198 9bdd47909ea8
parent 32104 d1d98a02473e
child 32590 95f4f08f950f
     1.1 --- a/src/Pure/thm.ML	Sun Jul 26 13:12:52 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Sun Jul 26 13:12:53 2009 +0200
     1.3 @@ -110,6 +110,7 @@
     1.4    val dest_arg1: cterm -> cterm
     1.5    val dest_abs: string option -> cterm -> cterm * cterm
     1.6    val capply: cterm -> cterm -> cterm
     1.7 +  val cabs_name: string * cterm -> cterm -> cterm
     1.8    val cabs: cterm -> cterm -> cterm
     1.9    val adjust_maxidx_cterm: int -> cterm -> cterm
    1.10    val incr_indexes_cterm: int -> cterm -> cterm
    1.11 @@ -274,16 +275,18 @@
    1.12        else raise CTERM ("capply: types don't agree", [cf, cx])
    1.13    | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
    1.14  
    1.15 -fun cabs
    1.16 -  (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
    1.17 +fun cabs_name
    1.18 +  (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
    1.19    (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
    1.20 -    let val t = Term.lambda t1 t2 in
    1.21 +    let val t = Term.lambda_name (x, t1) t2 in
    1.22        Cterm {thy_ref = merge_thys0 ct1 ct2,
    1.23          t = t, T = T1 --> T2,
    1.24          maxidx = Int.max (maxidx1, maxidx2),
    1.25          sorts = Sorts.union sorts1 sorts2}
    1.26      end;
    1.27  
    1.28 +fun cabs t u = cabs_name ("", t) u;
    1.29 +
    1.30  
    1.31  (* indexes *)
    1.32