--- a/src/Pure/conjunction.ML Wed Oct 28 16:25:10 2009 +0100
+++ b/src/Pure/conjunction.ML Wed Oct 28 16:25:26 2009 +0100
@@ -83,15 +83,16 @@
in
-val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
+val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
+val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
-val conjunctionI = Drule.store_standard_thm "conjunctionI"
- (Drule.implies_intr_list [A, B]
- (Thm.equal_elim
- (Thm.symmetric conjunction_def)
- (Thm.forall_intr C (Thm.implies_intr ABC
- (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
+val conjunctionI =
+ Drule.store_standard_thm (Binding.name "conjunctionI")
+ (Drule.implies_intr_list [A, B]
+ (Thm.equal_elim
+ (Thm.symmetric conjunction_def)
+ (Thm.forall_intr C (Thm.implies_intr ABC
+ (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
fun intr tha thb =