--- a/src/ZF/ex/bt.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/bt.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -17,7 +17,7 @@
 	  ["Lf : bt(A)",
 	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 val [LfI, BrI] = BT.intrs;