Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
authorwenzelm
Tue Mar 10 22:49:56 2009 +0100 (2009-03-10 ago)
changeset 30424692279df7cc2
parent 30423 6baef860dfa6
child 30426 699afca33527
Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
src/Pure/Isar/proof_context.ML
src/Pure/consts.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:27:32 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:49:56 2009 +0100
     1.3 @@ -262,9 +262,11 @@
     1.4  
     1.5  fun transfer_syntax thy =
     1.6    map_syntax (LocalSyntax.rebuild thy) #>
     1.7 -  map_consts (fn (local_consts, _) =>
     1.8 -    let val thy_consts = Sign.consts_of thy
     1.9 -    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
    1.10 +  map_consts (fn consts as (local_consts, global_consts) =>
    1.11 +    let val thy_consts = Sign.consts_of thy in
    1.12 +      if Consts.eq_consts (thy_consts, global_consts) then consts
    1.13 +      else (Consts.merge (local_consts, thy_consts), thy_consts)
    1.14 +    end);
    1.15  
    1.16  fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
    1.17  
     2.1 --- a/src/Pure/consts.ML	Tue Mar 10 22:27:32 2009 +0100
     2.2 +++ b/src/Pure/consts.ML	Tue Mar 10 22:49:56 2009 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  signature CONSTS =
     2.5  sig
     2.6    type T
     2.7 +  val eq_consts: T * T -> bool
     2.8    val abbrevs_of: T -> string list -> (term * term) list
     2.9    val dest: T ->
    2.10     {constants: (typ * term option) NameSpace.table,
    2.11 @@ -53,6 +54,13 @@
    2.12    constraints: typ Symtab.table,
    2.13    rev_abbrevs: (term * term) list Symtab.table};
    2.14  
    2.15 +fun eq_consts
    2.16 +   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    2.17 +    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
    2.18 +  pointer_eq (decls1, decls2) andalso
    2.19 +  pointer_eq (constraints1, constraints2) andalso
    2.20 +  pointer_eq (rev_abbrevs1, rev_abbrevs2);
    2.21 +
    2.22  fun make_consts (decls, constraints, rev_abbrevs) =
    2.23    Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
    2.24