IMP/Equiv.ML

--- a/IMP/Equiv.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/IMP/Equiv.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -9,13 +9,13 @@
 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
-val aexp_iff = store_thm("aexp_iff", result() RS spec);
+bind_thm("aexp_iff", result() RS spec);
 
 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))";
 by (bexp.induct_tac "b" 1);
 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
               addsimps (aexp_iff::B_simps@evalb_simps))));
-val bexp_iff = store_thm("bexp_iff", result() RS spec);
+bind_thm("bexp_iff", result() RS spec);
 
 val bexp1 = bexp_iff RS iffD1;
 val bexp2 = bexp_iff RS iffD2;