# HG changeset patch
# User wenzelm
# Date 1394631434 -3600
# Node ID 8ae2965ddc80f4c334c5b34eeb2425380ed6449a
# Parent  564a7bee8652aa906b3a57eb69ace0ad3980c5d0
tuned signature;

diff -r 564a7bee8652 -r 8ae2965ddc80 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -33,10 +33,9 @@
 fun consts_of thy =
  let
    val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
-   val consts = Symtab.dest constants
  in
    map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
-     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts)
+     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) constants)
  end;
 
 
diff -r 564a7bee8652 -r 8ae2965ddc80 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -1229,14 +1229,14 @@
 fun pretty_abbrevs show_globals ctxt =
   let
     val space = const_space ctxt;
-    val (constants, globals) =
+    val (constants, global_constants) =
       pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
+    val globals = Symtab.make global_constants;
     fun add_abbr (_, (_, NONE)) = I
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs =
-      Name_Space.markup_entries ctxt space (Symtab.fold add_abbr constants []);
+    val abbrevs = Name_Space.markup_entries ctxt space (fold add_abbr constants []);
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
diff -r 564a7bee8652 -r 8ae2965ddc80 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -108,8 +108,7 @@
       fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
 
     val matches =
-      Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
-        constants []
+      fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
       |> map (apsnd fst o snd);
   in
diff -r 564a7bee8652 -r 8ae2965ddc80 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/Pure/consts.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -13,8 +13,8 @@
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
    {const_space: Name_Space.T,
-    constants: (typ * term option) Symtab.table,
-    constraints: typ Symtab.table}
+    constants: (string * (typ * term option)) list,
+    constraints: (string * typ) list}
   val the_const: T -> string -> string * typ                   (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
@@ -89,8 +89,8 @@
  {const_space = Name_Space.space_of_table decls,
   constants =
     Name_Space.fold_table (fn (c, ({T, ...}, abbr)) =>
-      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty,
-  constraints = constraints};
+      cons (c, (T, Option.map #rhs abbr))) decls [],
+  constraints = Symtab.dest constraints};
 
 
 (* lookup consts *)
diff -r 564a7bee8652 -r 8ae2965ddc80 src/Pure/display.ML
--- a/src/Pure/display.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/Pure/display.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -168,11 +168,11 @@
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     val cnsts =
       Name_Space.markup_entries ctxt const_space
-        (filter_out (prune_const o fst) (Symtab.dest constants));
+        (filter_out (prune_const o fst) constants);
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
+    val cnstrs = Name_Space.markup_entries ctxt const_space constraints;
 
     val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
 
diff -r 564a7bee8652 -r 8ae2965ddc80 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Mar 12 14:23:26 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Mar 12 14:37:14 2014 +0100
@@ -876,8 +876,9 @@
 fun read_const_exprs_internal ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-      (#constants (Consts.dest (Sign.consts_of thy'))) [];
+    fun consts_of thy' =
+      fold (fn (c, (_, NONE)) => cons c | _ => I)
+        (#constants (Consts.dest (Sign.consts_of thy'))) [];
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');