# HG changeset patch
# User wenzelm
# Date 936213682 -7200
# Node ID c63d619286a3b144eec228fc5726a448b280460f
# Parent  0577bb18b1abc15346b409d893d05278bd5b370e
bind_thm;

diff -r 0577bb18b1ab -r c63d619286a3 src/FOL/FOL_lemmas1.ML
--- a/src/FOL/FOL_lemmas1.ML	Wed Sep 01 21:21:01 1999 +0200
+++ b/src/FOL/FOL_lemmas1.ML	Wed Sep 01 21:21:22 1999 +0200
@@ -7,7 +7,7 @@
 *)
 
 val classical = thm "classical";
-val ccontr = FalseE RS classical;
+bind_thm ("ccontr", FalseE RS classical);
 
 
 (*** Classical introduction rules for | and EX ***)
diff -r 0577bb18b1ab -r c63d619286a3 src/FOL/IFOL_lemmas.ML
--- a/src/FOL/IFOL_lemmas.ML	Wed Sep 01 21:21:01 1999 +0200
+++ b/src/FOL/IFOL_lemmas.ML	Wed Sep 01 21:21:22 1999 +0200
@@ -251,7 +251,7 @@
  (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
 
 (** ~ b=a ==> ~ a=b **)
-val [not_sym] = compose(sym,2,contrapos);
+bind_thm ("not_sym", hd (compose(sym,2,contrapos)));
 
 
 (* Two theorms for rewriting only one instance of a definition:
@@ -358,7 +358,7 @@
                (explode"PQRS"));
 
 (*special case for the equality predicate!*)
-val eq_cong = read_instantiate [("P","op =")] pred2_cong;
+bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong);
 
 
 (*** Simplifications of assumed implications.