--- a/src/HOL/Main.thy Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/Main.thy Tue Jul 12 11:51:31 2005 +0200
@@ -19,6 +19,12 @@
types_code
"bool" ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i = one_of [false, true];
+*}
consts_code
"True" ("true")
@@ -28,18 +34,14 @@
"op &" ("(_ andalso/ _)")
"HOL.If" ("(if _/ then _/ else _)")
- "wfrec" ("wf'_rec?")
+ "wfrec" ("\<module>wf'_rec?")
+attach {*
+fun wf_rec f x = f (wf_rec f) x;
+*}
quickcheck_params [default_type = int]
-(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
ML {*
-fun wf_rec f x = f (wf_rec f) x;
-
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-val term_of_int = HOLogic.mk_int o IntInf.fromInt;
-fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
-
local
fun eq_codegen thy defs gr dep thyname b t =
@@ -62,20 +64,6 @@
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
end;
-
-fun gen_bool i = one_of [false, true];
-
-fun gen_int i = one_of [~1, 1] * random_range 0 i;
-
-fun gen_fun_type _ G i =
- let
- val f = ref (fn x => raise ERROR);
- val _ = (f := (fn x =>
- let
- val y = G i;
- val f' = !f
- in (f := (fn x' => if x = x' then y else f' x'); y) end))
- in (fn x => !f x) end;
*}
setup eq_codegen_setup