bind_thm "ccontr";

--- a/src/HOL/HOL_lemmas.ML	Mon Oct 11 20:42:06 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Mon Oct 11 20:43:38 1999 +0200
@@ -264,7 +264,7 @@
     rtac (impI RS prem RS eqTrueI) 1,
     etac subst 1,  assume_tac 1]);
 
-val ccontr = FalseE RS classical;
+bind_thm ("ccontr", FalseE RS classical);
 
 (*Double negation law*)
 Goal "~~P ==> P";