# HG changeset patch
# User berghofe
# Date 1056914955 -7200
# Node ID c69d5bf3047d2fb30b50305ac2aaf067a0531b2b
# Parent  6c0f67e2f8d5e0f44b921c921204e2e488016a97
Moved function for renaming bound variables to Pure/drule.ML

diff -r 6c0f67e2f8d5 -r c69d5bf3047d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Jun 29 21:28:13 2003 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Jun 29 21:29:15 2003 +0200
@@ -263,26 +263,8 @@
 
 (* 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;
+  (Scan.lift (Scan.repeat Args.name_dummy >> (apsnd o Drule.rename_bvars'))) src;
 
 
 (* unfold / fold definitions *)