--- a/src/Pure/consts.ML Tue Mar 11 21:58:41 2014 +0100
+++ b/src/Pure/consts.ML Tue Mar 11 22:49:28 2014 +0100
@@ -9,6 +9,7 @@
sig
type T
val eq_consts: T * T -> bool
+ val change_base: bool -> T -> T
val retrieve_abbrevs: T -> string list -> term -> (term * term) list
val dest: T ->
{const_space: Name_Space.T,
@@ -65,6 +66,9 @@
fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
make_consts (f (decls, constraints, rev_abbrevs));
+fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
+ (Name_Space.change_base begin decls, constraints, rev_abbrevs));
+
(* reverted abbrevs *)