src/HOL/Main.thy

--- a/src/HOL/Main.thy	Tue May 27 17:39:17 2003 +0200
+++ b/src/HOL/Main.thy	Tue May 27 17:39:43 2003 +0200
@@ -44,6 +44,7 @@
 
 val term_of_list = HOLogic.mk_list;
 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;
 *}
 
 lemma [code]: "((n::nat) < 0) = False" by simp