--- a/src/HOL/Main.thy Fri Dec 10 16:48:01 2004 +0100
+++ b/src/HOL/Main.thy Fri Dec 10 16:48:29 2004 +0100
@@ -19,7 +19,6 @@
types_code
"bool" ("bool")
- "*" ("(_ */ _)")
consts_code
"True" ("true")
@@ -29,10 +28,6 @@
"op &" ("(_ andalso/ _)")
"If" ("(if _/ then _/ else _)")
- "Pair" ("(_,/ _)")
- "fst" ("fst")
- "snd" ("snd")
-
"wfrec" ("wf'_rec?")
quickcheck_params [default_type = int]
@@ -42,7 +37,6 @@
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
val term_of_int = HOLogic.mk_int;
-fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
@@ -65,8 +59,6 @@
fun gen_int i = one_of [~1, 1] * random_range 0 i;
-fun gen_id_42 aG bG i = (aG i, bG i);
-
fun gen_fun_type _ G i =
let
val f = ref (fn x => raise ERROR);