# HG changeset patch
# User haftmann
# Date 1147162157 -7200
# Node ID d68dd20af31fe7726ecb2532900e4ca0b87f7cfa
# Parent  8ced57ffc090c229d10081f977225a1e40b77fca
different object logic setup for CodegenTheorems

diff -r 8ced57ffc090 -r d68dd20af31f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 09 10:08:20 2006 +0200
+++ b/src/HOL/HOL.thy	Tue May 09 10:09:17 2006 +0200
@@ -1391,20 +1391,8 @@
 
 subsection {* Code generator setup *}
 
-ML {*
-val _ =
-  let
-    fun true_tac [] = (ALLGOALS o resolve_tac) [TrueI];
-    fun false_tac [false_asm] = (ALLGOALS o resolve_tac) [FalseE] THEN (ALLGOALS o resolve_tac) [false_asm]
-    fun and_tac impls = (ALLGOALS o resolve_tac) [conjI]
-        THEN (ALLGOALS o resolve_tac) impls;
-    fun eq_tac [] = (ALLGOALS o resolve_tac o single
-      o PureThy.get_thm (the_context ()) o Name) "HOL.atomize_eq";
-  in
-    CodegenTheorems.init_obj (the_context ())
-      "bool" ("True", true_tac) ("False", false_tac)
-        ("op &", and_tac) ("op =", eq_tac)
-  end;
+setup {*
+  CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
 *}
 
 code_alias