test/Tools/isac/ProgLang/evaluate.sml
changeset 60407 eca042e683b9
parent 60405 d4ebe139100d
child 60424 c3acf9c442ac
     1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 23 13:47:16 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Fri Sep 24 14:18:10 2021 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4  "~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
     1.5      val simp_ctxt =
     1.6        Proof_Context.init_global thy
     1.7 -      |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
     1.8 +      |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
     1.9      val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
    1.10  
    1.11  if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";