make name table work the way it was intended to
authorblanchet
Thu Jan 10 23:34:20 2013 +0100 (2013-01-10 ago)
changeset 5081541b804049fae
parent 50814 4247cbd78aaf
child 50816 2c366a03c888
make name table work the way it was intended to
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 10 23:34:19 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 10 23:34:20 2013 +0100
     1.3 @@ -344,12 +344,12 @@
     1.4    let
     1.5      fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
     1.6      fun add_plain canon alias =
     1.7 -      Symtab.update (Thm.get_name_hint canon,
     1.8 +      Symtab.update (Thm.get_name_hint alias,
     1.9                       name_of (if_thm_before canon alias))
    1.10      fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
    1.11      fun add_inclass (name, target) =
    1.12        fold (fn s => Symtab.update (s, target)) (un_class_ify name)
    1.13 -    val prop_tab = fold_rev cons_thm facts Termtab.empty
    1.14 +    val prop_tab = fold cons_thm facts Termtab.empty
    1.15      val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
    1.16      val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
    1.17    in (plain_name_tab, inclass_name_tab) end