# HG changeset patch
# User wenzelm
# Date 1248606773 -7200
# Node ID 9bdd47909ea894a6749a452f1f00e8d4bd27d593
# Parent  bc341bbe4417ebbfaa2e9080e90342ea2f920ebe
lambda/cabs/all: named variants;

diff -r bc341bbe4417 -r 9bdd47909ea8 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Jul 26 13:12:52 2009 +0200
+++ b/src/Pure/more_thm.ML	Sun Jul 26 13:12:53 2009 +0200
@@ -11,6 +11,8 @@
   include THM
   val aconvc: cterm * cterm -> bool
   val add_cterm_frees: cterm -> cterm list -> cterm list
+  val all_name: string * cterm -> cterm -> cterm
+  val all: cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm
   val dest_implies: cterm -> cterm * cterm
@@ -102,6 +104,14 @@
 
 (* cterm constructors and destructors *)
 
+fun all_name (x, t) A =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_cterm t);
+    val T = #T (Thm.rep_cterm t);
+  in Thm.capply (cert (Const ("all", (T --> propT) --> propT))) (Thm.cabs_name (x, t) A) end;
+
+fun all t A = all_name ("", t) A;
+
 fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
 fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
 
diff -r bc341bbe4417 -r 9bdd47909ea8 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Jul 26 13:12:52 2009 +0200
+++ b/src/Pure/term.ML	Sun Jul 26 13:12:53 2009 +0200
@@ -151,6 +151,7 @@
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
+  val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
@@ -719,14 +720,15 @@
         | _ => raise Same.SAME);
   in abs 0 body handle Same.SAME => body end;
 
-fun lambda v t =
-  let val x =
-    (case v of
-      Const (x, _) => Long_Name.base_name x
-    | Free (x, _) => x
-    | Var ((x, _), _) => x
-    | _ => Name.uu)
-  in Abs (x, fastype_of v, abstract_over (v, t)) end;
+fun term_name (Const (x, _)) = Long_Name.base_name x
+  | term_name (Free (x, _)) = x
+  | term_name (Var ((x, _), _)) = x
+  | term_name _ = Name.uu;
+
+fun lambda_name (x, v) t =
+  Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
+
+fun lambda v t = lambda_name ("", v) t;
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
diff -r bc341bbe4417 -r 9bdd47909ea8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Jul 26 13:12:52 2009 +0200
+++ b/src/Pure/thm.ML	Sun Jul 26 13:12:53 2009 +0200
@@ -110,6 +110,7 @@
   val dest_arg1: cterm -> cterm
   val dest_abs: string option -> cterm -> cterm * cterm
   val capply: cterm -> cterm -> cterm
+  val cabs_name: string * cterm -> cterm -> cterm
   val cabs: cterm -> cterm -> cterm
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val incr_indexes_cterm: int -> cterm -> cterm
@@ -274,16 +275,18 @@
       else raise CTERM ("capply: types don't agree", [cf, cx])
   | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
 
-fun cabs
-  (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
+fun cabs_name
+  (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
-    let val t = Term.lambda t1 t2 in
+    let val t = Term.lambda_name (x, t1) t2 in
       Cterm {thy_ref = merge_thys0 ct1 ct2,
         t = t, T = T1 --> T2,
         maxidx = Int.max (maxidx1, maxidx2),
         sorts = Sorts.union sorts1 sorts2}
     end;
 
+fun cabs t u = cabs_name ("", t) u;
+
 
 (* indexes *)