src/ZF/subset.ML

--- a/src/ZF/subset.ML	Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/subset.ML	Wed Dec 14 11:41:49 1994 +0100
@@ -24,7 +24,7 @@
 
 (*A safe special case of subset elimination, adding no new variables 
   [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
-val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE);
+bind_thm ("cons_subsetE", (cons_subset_iff RS iffD1 RS conjE));
 
 qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
  (fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);