diff -r af32e2c3f77a -r a6922171b396 src/ZF/Coind/ECR.ML
--- a/src/ZF/Coind/ECR.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/ECR.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -24,11 +24,9 @@
 
 (* Specialised elimination rules *)
 
-val htr_constE = 
-  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
+val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
 
-val htr_closE =
-  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
+val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
 
 (* Classical reasoning sets *)