implemented MaSh/SML hints
authorblanchet
Tue May 20 09:57:10 2014 +0200 (2014-05-20)
changeset 57014b7999893ffcc
parent 57013 ed95456499e6
child 57015 842bb6d36263
child 57021 6a8fd2ac6756
implemented MaSh/SML hints
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 09:38:39 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 09:57:10 2014 +0200
     1.3 @@ -448,12 +448,12 @@
     1.4      val visible_fact_set = Symtab.make_set visible_facts
     1.5  
     1.6      val all_nodes =
     1.7 -      Graph.schedule (K I) access_G
     1.8 -      |> List.partition (Symtab.defined visible_fact_set o fst)
     1.9 -      |> op @
    1.10 +      (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
    1.11 +       |> List.partition (Symtab.defined visible_fact_set o #1) |> op @) @
    1.12 +      (if null hints then [] else [(".goal", feats, hints)])
    1.13  
    1.14      val (rev_depss, featss, (_, _, rev_facts), (num_feats, feat_tab, _)) =
    1.15 -      fold (fn (fact, (_, feats, deps)) =>
    1.16 +      fold (fn (fact, feats, deps) =>
    1.17              fn (depss, featss, fact_xtab as (_, fact_tab, _), feat_xtab) =>
    1.18            let
    1.19              fun add_feat (feat, weight) (xtab as (n, tab, _)) =