tuned signature;
authorwenzelm
Wed Mar 12 14:37:14 2014 +0100 (2014-03-12)
changeset 560628ae2965ddc80
parent 56061 564a7bee8652
child 56063 38f13d055107
tuned signature;
src/HOL/Mutabelle/mutabelle.ML
src/Pure/Isar/proof_context.ML
src/Pure/Tools/find_consts.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 12 14:23:26 2014 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 12 14:37:14 2014 +0100
     1.3 @@ -33,10 +33,9 @@
     1.4  fun consts_of thy =
     1.5   let
     1.6     val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
     1.7 -   val consts = Symtab.dest constants
     1.8   in
     1.9     map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
    1.10 -     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts)
    1.11 +     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) constants)
    1.12   end;
    1.13  
    1.14  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 12 14:23:26 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 12 14:37:14 2014 +0100
     2.3 @@ -1229,14 +1229,14 @@
     2.4  fun pretty_abbrevs show_globals ctxt =
     2.5    let
     2.6      val space = const_space ctxt;
     2.7 -    val (constants, globals) =
     2.8 +    val (constants, global_constants) =
     2.9        pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
    2.10 +    val globals = Symtab.make global_constants;
    2.11      fun add_abbr (_, (_, NONE)) = I
    2.12        | add_abbr (c, (T, SOME t)) =
    2.13            if not show_globals andalso Symtab.defined globals c then I
    2.14            else cons (c, Logic.mk_equals (Const (c, T), t));
    2.15 -    val abbrevs =
    2.16 -      Name_Space.markup_entries ctxt space (Symtab.fold add_abbr constants []);
    2.17 +    val abbrevs = Name_Space.markup_entries ctxt space (fold add_abbr constants []);
    2.18    in
    2.19      if null abbrevs then []
    2.20      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
     3.1 --- a/src/Pure/Tools/find_consts.ML	Wed Mar 12 14:23:26 2014 +0100
     3.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Mar 12 14:37:14 2014 +0100
     3.3 @@ -108,8 +108,7 @@
     3.4        fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
     3.5  
     3.6      val matches =
     3.7 -      Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
     3.8 -        constants []
     3.9 +      fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
    3.10        |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
    3.11        |> map (apsnd fst o snd);
    3.12    in
     4.1 --- a/src/Pure/consts.ML	Wed Mar 12 14:23:26 2014 +0100
     4.2 +++ b/src/Pure/consts.ML	Wed Mar 12 14:37:14 2014 +0100
     4.3 @@ -13,8 +13,8 @@
     4.4    val retrieve_abbrevs: T -> string list -> term -> (term * term) list
     4.5    val dest: T ->
     4.6     {const_space: Name_Space.T,
     4.7 -    constants: (typ * term option) Symtab.table,
     4.8 -    constraints: typ Symtab.table}
     4.9 +    constants: (string * (typ * term option)) list,
    4.10 +    constraints: (string * typ) list}
    4.11    val the_const: T -> string -> string * typ                   (*exception TYPE*)
    4.12    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
    4.13    val type_scheme: T -> string -> typ                          (*exception TYPE*)
    4.14 @@ -89,8 +89,8 @@
    4.15   {const_space = Name_Space.space_of_table decls,
    4.16    constants =
    4.17      Name_Space.fold_table (fn (c, ({T, ...}, abbr)) =>
    4.18 -      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty,
    4.19 -  constraints = constraints};
    4.20 +      cons (c, (T, Option.map #rhs abbr))) decls [],
    4.21 +  constraints = Symtab.dest constraints};
    4.22  
    4.23  
    4.24  (* lookup consts *)
     5.1 --- a/src/Pure/display.ML	Wed Mar 12 14:23:26 2014 +0100
     5.2 +++ b/src/Pure/display.ML	Wed Mar 12 14:37:14 2014 +0100
     5.3 @@ -168,11 +168,11 @@
     5.4      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     5.5      val cnsts =
     5.6        Name_Space.markup_entries ctxt const_space
     5.7 -        (filter_out (prune_const o fst) (Symtab.dest constants));
     5.8 +        (filter_out (prune_const o fst) constants);
     5.9  
    5.10      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    5.11      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    5.12 -    val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
    5.13 +    val cnstrs = Name_Space.markup_entries ctxt const_space constraints;
    5.14  
    5.15      val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
    5.16  
     6.1 --- a/src/Tools/Code/code_thingol.ML	Wed Mar 12 14:23:26 2014 +0100
     6.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Mar 12 14:37:14 2014 +0100
     6.3 @@ -876,8 +876,9 @@
     6.4  fun read_const_exprs_internal ctxt =
     6.5    let
     6.6      val thy = Proof_Context.theory_of ctxt;
     6.7 -    fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
     6.8 -      (#constants (Consts.dest (Sign.consts_of thy'))) [];
     6.9 +    fun consts_of thy' =
    6.10 +      fold (fn (c, (_, NONE)) => cons c | _ => I)
    6.11 +        (#constants (Consts.dest (Sign.consts_of thy'))) [];
    6.12      fun belongs_here thy' c = forall
    6.13        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
    6.14      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');