--- BilbyFs_CorresProof.thy	2015-11-17 21:58:57.050814378 +1100
+++ BilbyFs_CorresProof.thy	2015-11-17 22:00:43.698453529 +1100
@@ -466,6 +466,12 @@
 (* Additional Let rule for programs in K-normal form *)
 lemmas corres_nested_let = corres_nested_let_base[OF LET_TRUE_def]
 (* Run proofs for generated functions *)
+
+(* BilbyFs needs this for some reason *)
+end (* context BilbyFs *)
+declare [[unify_search_bound=999, unify_trace_bound=999]]
+context BilbyFs begin
+
 (* ML{*
 fun all_corres_goals corres_tac typing_tree_of time_limit ctxt (tab : obligations) =
   let