# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID 8a8d71e34297f8c4b2cb1837343c23d3a78182e8
# Parent  c552d7f1720ba400d0714f0707db759c3901c8a8
fixed MaSh state load code so it works even if the facts are read in disorder

diff -r c552d7f1720b -r 8a8d71e34297 src/HOL/TPTP/MaSh_Eval.thy
--- 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} []
 *}
diff -r c552d7f1720b -r 8a8d71e34297 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- 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)