src/HOL/Main.thy
changeset 15965 f422f8283491
parent 15872 8336ff711d80
child 16587 b34c8aa657a5
     1.1 --- a/src/HOL/Main.thy	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -32,11 +32,12 @@
     1.4  
     1.5  quickcheck_params [default_type = int]
     1.6  
     1.7 +(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
     1.8  ML {*
     1.9  fun wf_rec f x = f (wf_rec f) x;
    1.10  
    1.11  fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.12 -val term_of_int = HOLogic.mk_int;
    1.13 +val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    1.14  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    1.15  
    1.16  val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"