Skip to content
Permalink
Browse files

Remove a bug from ml_translatorLib.clean_v_thms

  • Loading branch information...
myreen committed Sep 7, 2019
1 parent 26f4bae commit a8e2240b45c8f858615a65f130198101bb07e6b6
Showing with 2 additions and 2 deletions.
  1. +2 −1 translator/ml_translatorLib.sml
  2. +0 −1 translator/ml_translator_testScript.sml
@@ -4617,7 +4617,8 @@ val state = state'
fun clean_v_thms () = let
val inst_env = INST [env_tm |-> get_curr_env()]
fun can_lookup_constant (_,_,c_tm,_,_,_) =
can clean_assumptions_quietly (D (inst_env (hol2deep c_tm)))
((can clean_assumptions_quietly (D (inst_env (lookup_v_thm c_tm))))
handle Interrupt => raise Interrupt | _ => false)
val delete_count = filter_v_thms can_lookup_constant
in if delete_count < 1 then () else
print ("Removed " ^ int_to_string delete_count ^
@@ -436,5 +436,4 @@ val res = translate TAKE_def;
val res = translate DROP_def;
val res = translate chop_str_def

val _ = filter_v_thms (fn (n,_,_,_,_,_) => not (String.isPrefix "test" n));
val _ = export_theory();

0 comments on commit a8e2240

Please sign in to comment.
You can’t perform that action at this time.