src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Pure/simplifier.ML	Wed Jun 06 18:19:55 2018 +0200
@@ -32,7 +32,7 @@
   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
   val simp_add: attribute
   val simp_del: attribute
-  val simp_reorient: attribute
+  val simp_flip: attribute
   val cong_add: attribute
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string
@@ -90,7 +90,7 @@
 
 val simp_add = attrib add_simp;
 val simp_del = attrib del_simp;
-val simp_reorient = attrib reorient_simp;
+val simp_flip = attrib flip_simp;
 val cong_add = attrib add_cong;
 val cong_del = attrib del_cong;
 
@@ -269,7 +269,7 @@
 (* add / del *)
 
 val simpN = "simp";
-val reorientN = "reorient"
+val flipN = "flip"
 val congN = "cong";
 val onlyN = "only";
 val no_asmN = "no_asm";
@@ -343,7 +343,7 @@
  [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
-  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
+  Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
@@ -351,7 +351,7 @@
 val simp_modifiers' =
  [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
-  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
+  Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;