diff --git a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml index 246345e9da..a630675701 100644 --- a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml +++ b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml @@ -11,7 +11,8 @@ val confs = LIST_CONJ to_dataBootstrapTheory.bvi_conf_def] val encode_backend_config_cake_config_lemma = - “encode_backend_config (config_to_inc_config cake_config)” + “encode_backend_config $ config_to_inc_config $ cake_config with <| + word_to_word_conf := (cake_config.word_to_word_conf with reg_alg := 4) |>” |> (SIMP_CONV (srw_ss()) [cake_config_def,confs,encode_backend_config_def] THENC EVAL); Definition config_enc_str_def: