--- a/src/Pure/conjunction.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/conjunction.ML Sun Apr 06 15:43:45 2014 +0200
@@ -84,11 +84,14 @@
in
-val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
+val conjunctionD1 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1);
+
+val conjunctionD2 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2);
val conjunctionI =
- Drule.store_standard_thm (Binding.name "conjunctionI")
+ Drule.store_standard_thm (Binding.make ("conjunctionI", @{here}))
(Drule.implies_intr_list [A, B]
(Thm.equal_elim
(Thm.symmetric conjunction_def)