fixed MaSh state load code so it works even if the facts are read in disorder

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:04 2012 +0200
@@ -20,7 +20,7 @@
 *}
 
 ML {*
-val do_it = true (* switch to "true" to generate the files *);
+val do_it = false (* switch to "true" to generate the files *);
 val thy = @{theory Nat};
 val params = Sledgehammer_Isar.default_params @{context} []
 *}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -432,17 +432,20 @@
          SOME (comp_thys :: incomp_thys :: fact_lines) =>
          let
            fun add_thy comp thy = Symtab.update (thy, comp)
+           fun add_edge_to name parent =
+             Graph.default_node (parent, ())
+             #> Graph.add_edge (parent, name)
            fun add_fact_line line =
              case extract_query line of
                ("", _) => I (* shouldn't happen *)
              | (name, parents) =>
                Graph.default_node (name, ())
-               #> fold (fn par => Graph.add_edge (par, name)) parents
+               #> fold (add_edge_to name) parents
            val thys =
              Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
                           |> fold (add_thy false) (unescape_metas incomp_thys)
            val fact_graph =
-             try_graph ctxt "loading state file" Graph.empty (fn () =>
+             try_graph ctxt "loading state" Graph.empty (fn () =>
                  Graph.empty |> fold add_fact_line fact_lines)
          in {thys = thys, fact_graph = fact_graph} end
        | _ => empty_state)