src/Pure/sign.ML
changeset 56056 4d46d53566e6
parent 56026 893fe12639bc
child 56057 ad6bd8030d88
     1.1 --- a/src/Pure/sign.ML	Tue Mar 11 21:58:41 2014 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 11 22:49:28 2014 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  
     1.5  signature SIGN =
     1.6  sig
     1.7 +  val change_begin: theory -> theory
     1.8 +  val change_end: theory -> theory
     1.9 +  val change_end_local: Proof.context -> Proof.context
    1.10    val syn_of: theory -> Syntax.syntax
    1.11    val tsig_of: theory -> Type.tsig
    1.12    val classes_of: theory -> Sorts.algebra
    1.13 @@ -151,6 +154,18 @@
    1.14  fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
    1.15  
    1.16  
    1.17 +(* linear change discipline *)
    1.18 +
    1.19 +fun change_base begin = map_sign (fn (syn, tsig, consts) =>
    1.20 +  (syn, Type.change_base begin tsig, Consts.change_base begin consts));
    1.21 +
    1.22 +val change_begin = change_base true;
    1.23 +val change_end = change_base false;
    1.24 +
    1.25 +fun change_end_local ctxt =
    1.26 +  Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt;
    1.27 +
    1.28 +
    1.29  (* syntax *)
    1.30  
    1.31  val syn_of = #syn o rep_sg;