--- 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 *)