# HG changeset patch
# User blanchet
# Date 1400572630 -7200
# Node ID b7999893ffcce9eff092d66553d4cbb92c823185
# Parent  ed95456499e6714fad842aaefa228dd1fb25115c
implemented MaSh/SML hints

diff -r ed95456499e6 -r b7999893ffcc src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 09:38:39 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 09:57:10 2014 +0200
@@ -448,12 +448,12 @@
     val visible_fact_set = Symtab.make_set visible_facts
 
     val all_nodes =
-      Graph.schedule (K I) access_G
-      |> List.partition (Symtab.defined visible_fact_set o fst)
-      |> op @
+      (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
+       |> List.partition (Symtab.defined visible_fact_set o #1) |> op @) @
+      (if null hints then [] else [(".goal", feats, hints)])
 
     val (rev_depss, featss, (_, _, rev_facts), (num_feats, feat_tab, _)) =
-      fold (fn (fact, (_, feats, deps)) =>
+      fold (fn (fact, feats, deps) =>
             fn (depss, featss, fact_xtab as (_, fact_tab, _), feat_xtab) =>
           let
             fun add_feat (feat, weight) (xtab as (n, tab, _)) =