src/HOL/Main.thy

--- a/src/HOL/Main.thy	Fri Jul 01 13:54:57 2005 +0200
+++ b/src/HOL/Main.thy	Fri Jul 01 13:56:34 2005 +0200
@@ -40,21 +40,28 @@
 val term_of_int = HOLogic.mk_int o IntInf.fromInt;
 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
 
-val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
-  (fn thy => fn gr => fn dep => fn b => fn t =>
+local
+
+fun eq_codegen thy defs gr dep thyname b t =
     (case strip_comb t of
        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
      | (Const ("op =", _), [t, u]) =>
           let
-            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
-            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
+            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
           in
             SOME (gr'', Codegen.parens
               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
           end
      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
-         thy dep b (gr, Codegen.eta_expand t ts 2))
-     | _ => NONE))];
+         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+     | _ => NONE);
+
+in
+
+val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
+
+end;
 
 fun gen_bool i = one_of [false, true];
 
@@ -73,9 +80,7 @@
 
 setup eq_codegen_setup
 
-lemma [code]: "((n::nat) < 0) = False" by simp
-lemma [code]: "(0 < Suc n) = True" by simp
-lemmas [code] = Suc_less_eq imp_conv_disj
+lemmas [code] = imp_conv_disj
 
 subsection {* Configuration of the 'refute' command *}