eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
authorwenzelm
Thu Mar 05 15:27:07 2009 +0100 (2009-03-05 ago)
changeset 30284907da436f8a9
parent 30283 520872460b7b
child 30285 a135bfab6e83
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
src/Pure/Isar/proof_context.ML
src/Pure/consts.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 05 15:25:35 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 05 15:27:07 2009 +0100
     1.3 @@ -263,11 +263,9 @@
     1.4  
     1.5  fun transfer_syntax thy =
     1.6    map_syntax (LocalSyntax.rebuild thy) #>
     1.7 -  map_consts (fn consts as (local_consts, global_consts) =>
     1.8 -    let val thy_consts = Sign.consts_of thy in
     1.9 -      if Consts.eq_consts (thy_consts, global_consts) then consts
    1.10 -      else (Consts.merge (local_consts, thy_consts), thy_consts)
    1.11 -    end);
    1.12 +  map_consts (fn (local_consts, _) =>
    1.13 +    let val thy_consts = Sign.consts_of thy
    1.14 +    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
    1.15  
    1.16  fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
    1.17  
     2.1 --- a/src/Pure/consts.ML	Thu Mar 05 15:25:35 2009 +0100
     2.2 +++ b/src/Pure/consts.ML	Thu Mar 05 15:27:07 2009 +0100
     2.3 @@ -8,7 +8,6 @@
     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 @@ -52,23 +51,21 @@
    2.12  datatype T = Consts of
    2.13   {decls: ((decl * abbrev option) * serial) NameSpace.table,
    2.14    constraints: typ Symtab.table,
    2.15 -  rev_abbrevs: (term * term) list Symtab.table} * stamp;
    2.16 -
    2.17 -fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2;
    2.18 +  rev_abbrevs: (term * term) list Symtab.table};
    2.19  
    2.20  fun make_consts (decls, constraints, rev_abbrevs) =
    2.21 -  Consts ({decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs}, stamp ());
    2.22 +  Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
    2.23  
    2.24 -fun map_consts f (Consts ({decls, constraints, rev_abbrevs}, _)) =
    2.25 +fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
    2.26    make_consts (f (decls, constraints, rev_abbrevs));
    2.27  
    2.28 -fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes =
    2.29 +fun abbrevs_of (Consts {rev_abbrevs, ...}) modes =
    2.30    maps (Symtab.lookup_list rev_abbrevs) modes;
    2.31  
    2.32  
    2.33  (* dest consts *)
    2.34  
    2.35 -fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
    2.36 +fun dest (Consts {decls = (space, decls), constraints, ...}) =
    2.37   {constants = (space,
    2.38      Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
    2.39        Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
    2.40 @@ -77,7 +74,7 @@
    2.41  
    2.42  (* lookup consts *)
    2.43  
    2.44 -fun the_const (Consts ({decls = (_, tab), ...}, _)) c =
    2.45 +fun the_const (Consts {decls = (_, tab), ...}) c =
    2.46    (case Symtab.lookup tab c of
    2.47      SOME (decl, _) => decl
    2.48    | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
    2.49 @@ -99,7 +96,7 @@
    2.50  
    2.51  val is_monomorphic = null oo type_arguments;
    2.52  
    2.53 -fun the_constraint (consts as Consts ({constraints, ...}, _)) c =
    2.54 +fun the_constraint (consts as Consts {constraints, ...}) c =
    2.55    (case Symtab.lookup constraints c of
    2.56      SOME T => T
    2.57    | NONE => type_scheme consts c);
    2.58 @@ -107,7 +104,7 @@
    2.59  
    2.60  (* name space and syntax *)
    2.61  
    2.62 -fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
    2.63 +fun space_of (Consts {decls = (space, _), ...}) = space;
    2.64  
    2.65  val intern = NameSpace.intern o space_of;
    2.66  val extern = NameSpace.extern o space_of;
    2.67 @@ -307,8 +304,8 @@
    2.68  val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
    2.69  
    2.70  fun merge
    2.71 -   (Consts ({decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, _),
    2.72 -    Consts ({decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}, _)) =
    2.73 +   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    2.74 +    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
    2.75    let
    2.76      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
    2.77        handle Symtab.DUP c => err_dup_const c;