Update CakeML to the latest compiling state

67de6c46 · Heiko Becker · 2611a9f2 · 67de6c46 · ffce1e98 · 120c3f18
Commit 67de6c46 authored Apr 17, 2018 by Heiko Becker
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 5 deletions

hol4/Infra/FloverTactics.sml hol4/Infra/FloverTactics.sml +2 -4

hol4/cakeml hol4/cakeml +1 -1

No files found.
--- a/hol4/Infra/FloverTactics.sml
+++ b/hol4/Infra/FloverTactics.sml
@@ -165,11 +165,9 @@ fun add_unevaluated_function (t:term) :unit =
  let
      val add_t = "val _ = FloverTactics.eval_funs :=``" ^ term_to_string t ^ "`` :: (!FloverTactics.eval_funs);"
      val _ = adjoin_to_theory
-                  { sig_ps =
-                    SOME (fn ppstrm => ()),
+                  { sig_ps = NONE,
                    struct_ps =
-                    SOME (fn ppstrm =>
-                             PP.add_string ppstrm add_t)};
+                    SOME (fn _ => PP.add_string add_t)};
  in
  eval_funs := t :: (!eval_funs)
  end;

--- a/cakeml @ ffce1e98
+++ b/cakeml @ ffce1e98
-Subproject commit 120c3f18b89f91ef6697c1f29d2025cbe2369b9a
+Subproject commit ffce1e98edd43af5f177e1c1cdb612e8c4ac7f29