From db1927bde6b56c8aa0c4a080795e6c33e4678b84 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 22 Apr 2015 05:53:24 +0100
Subject: [PATCH] translate anub (required MEMBER_INTRO for the induction thm)

---
 bootstrap/translation/repl/replMLScript.sml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/bootstrap/translation/repl/replMLScript.sml b/bootstrap/translation/repl/replMLScript.sml
index 1ae3b5e154..b1b74ec988 100644
--- a/bootstrap/translation/repl/replMLScript.sml
+++ b/bootstrap/translation/repl/replMLScript.sml
@@ -282,9 +282,11 @@ val ts_unify_side_def = store_thm("ts_unify_side_def",
   THEN FULL_SIMP_TAC std_ss [])
   |> update_precondition;
 
-
 (* type inference: rest *)
 
+val _ = save_thm("anub_ind",REWRITE_RULE[MEMBER_INTRO]miscTheory.anub_ind)
+val _ = translate (REWRITE_RULE[MEMBER_INTRO] miscTheory.anub_def)
+
 val _ = (extra_preprocessing :=
   [MEMBER_INTRO, MAP, OPTION_BIND_THM, st_ex_bind_def,
    st_ex_return_def, failwith_def, guard_def, read_def, write_def]);