src/Pure/conjunction.ML

   Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
 
 in
 
 val conjunctionD1 =
-  Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1);
+  Drule.store_standard_thm (Binding.make ("conjunctionD1", \<^here>)) (conjunctionD #1);
 
 val conjunctionD2 =
-  Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2);
+  Drule.store_standard_thm (Binding.make ("conjunctionD2", \<^here>)) (conjunctionD #2);
 
 val conjunctionI =
-  Drule.store_standard_thm (Binding.make ("conjunctionI", @{here}))
+  Drule.store_standard_thm (Binding.make ("conjunctionI", \<^here>))
     (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])))));