# HG changeset patch
# User berghofe
# Date 1042843974 -3600
# Node ID 44de406a72732aa0dc0eaedd268d25ffec139ccd
# Parent  ecb2df44253e6bf3d90076a4ceb42e3ee4bb1f9e
Added rename_abs attribute for renaming bound variables.

diff -r ecb2df44253e -r 44de406a7273 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jan 17 15:39:29 2003 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Jan 17 23:52:54 2003 +0100
@@ -261,6 +261,30 @@
 val of_local = gen_of I;
 
 
+(* rename_abs *)
+
+fun rename [] t = ([], t)
+  | rename (x' :: xs) (Abs (x, T, t)) =
+      let val (xs', t') = rename xs t
+      in (xs', Abs (if_none x' x, T, t')) end
+  | rename xs (t $ u) =
+      let
+        val (xs', t') = rename xs t;
+        val (xs'', u') = rename xs' u
+      in (xs'', t' $ u') end
+  | rename xs t = (xs, t);
+
+fun rename_abs_thm xs (ctxt, thm) =
+  let val {sign, prop, ...} = rep_thm thm;
+  in case rename xs prop of
+      ([], prop') => (ctxt, equal_elim (reflexive (cterm_of sign prop')) thm)
+    | _ => error "More names than abstractions in theorem"
+  end;
+
+fun rename_abs src = syntax
+  (Scan.lift (Scan.repeat Args.name_dummy >> rename_abs_thm)) src;
+
+
 (* unfold / fold definitions *)
 
 fun gen_rewrite rew defs (x, thm) = (x, rew defs thm);
@@ -338,6 +362,7 @@
   ("OF", (OF_global, OF_local), "rule applied to facts"),
   ("where", (where_global, where_local), "named instantiation of theorem"),
   ("of", (of_global, of_local), "rule applied to terms"),
+  ("rename_abs", (rename_abs, rename_abs), "rename bound variables in abstractions"),
   ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   ("folded", (folded_global, folded_local), "folded definitions"),
   ("standard", (standard, standard), "result put into standard form"),