1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 17 15:35:27 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 17 16:55:21 2009 +0100
     1.3 @@ -513,9 +513,11 @@
     1.4      val thy = theory_of ctxt;
     1.5      val consts = consts_of ctxt;
     1.6      val Mode {abbrev, ...} = get_mode ctxt;
     1.7 +    val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
     1.8 +    fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
     1.9    in
    1.10      if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
    1.11 -    else t |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) []
    1.12 +    else Pattern.rewrite_term thy [] [match_abbrev] t
    1.13    end;
    1.14  
    1.15  

     2.1 --- a/src/Pure/consts.ML	Tue Mar 17 15:35:27 2009 +0100
     2.2 +++ b/src/Pure/consts.ML	Tue Mar 17 16:55:21 2009 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  sig
     2.5    type T
     2.6    val eq_consts: T * T -> bool
     2.7 -  val abbrevs_of: T -> string list -> (term * term) list
     2.8 +  val retrieve_abbrevs: T -> string list -> term -> (term * term) list
     2.9    val dest: T ->
    2.10     {constants: (typ * term option) NameSpace.table,
    2.11      constraints: typ NameSpace.table}
    2.12 @@ -52,7 +52,7 @@
    2.13  datatype T = Consts of
    2.14   {decls: ((decl * abbrev option) * serial) NameSpace.table,
    2.15    constraints: typ Symtab.table,
    2.16 -  rev_abbrevs: (term * term) list Symtab.table};
    2.17 +  rev_abbrevs: (term * term) Item_Net.T Symtab.table};
    2.18  
    2.19  fun eq_consts
    2.20     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    2.21 @@ -67,8 +67,17 @@
    2.22  fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
    2.23    make_consts (f (decls, constraints, rev_abbrevs));
    2.24  
    2.25 -fun abbrevs_of (Consts {rev_abbrevs, ...}) modes =
    2.26 -  maps (Symtab.lookup_list rev_abbrevs) modes;
    2.27 +
    2.28 +(* reverted abbrevs *)
    2.29 +
    2.30 +val empty_abbrevs = Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
    2.31 +
    2.32 +fun insert_abbrevs mode abbrs =
    2.33 +  Symtab.map_default (mode, empty_abbrevs) (fold Item_Net.insert abbrs);
    2.34 +
    2.35 +fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
    2.36 +  let val nets = map_filter (Symtab.lookup rev_abbrevs) modes
    2.37 +  in fn t => maps (fn net => Item_Net.retrieve net t) nets end;
    2.38  
    2.39  
    2.40  (* dest consts *)
    2.41 @@ -291,7 +300,7 @@
    2.42          val (_, decls') = decls
    2.43            |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
    2.44          val rev_abbrevs' = rev_abbrevs
    2.45 -          |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
    2.46 +          |> insert_abbrevs mode (rev_abbrev lhs rhs);
    2.47        in (decls', constraints, rev_abbrevs') end)
    2.48      |> pair (lhs, rhs)
    2.49    end;
    2.50 @@ -300,7 +309,7 @@
    2.51    let
    2.52      val (T, rhs) = the_abbreviation consts c;
    2.53      val rev_abbrevs' = rev_abbrevs
    2.54 -      |> fold (curry Symtab.cons_list mode) (rev_abbrev (Const (c, T)) rhs);
    2.55 +      |> insert_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
    2.56    in (decls, constraints, rev_abbrevs') end);
    2.57  
    2.58  end;
    2.59 @@ -317,8 +326,7 @@
    2.60      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
    2.61        handle Symtab.DUP c => err_dup_const c;
    2.62      val constraints' = Symtab.join (K fst) (constraints1, constraints2);
    2.63 -    val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
    2.64 -      (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
    2.65 +    val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
    2.66    in make_consts (decls', constraints', rev_abbrevs') end;
    2.67  
    2.68  end;