--- a/src/Provers/simplifier.ML Wed Mar 08 23:46:59 2000 +0100
+++ b/src/Provers/simplifier.ML Wed Mar 08 23:47:44 2000 +0100
@@ -474,17 +474,19 @@
(* simplification *)
+val colon = Args.$$$ ":";
+
val simp_modifiers =
- [Args.$$$ simpN -- Args.$$$ addN >> K (I, simp_add_local),
- Args.$$$ simpN -- Args.$$$ delN >> K (I, simp_del_local),
- Args.$$$ simpN -- Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
- Args.$$$ otherN >> K (I, I)];
+ [Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
+ Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local),
+ Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
+ Args.$$$ otherN -- colon >> K (I, I)];
val simp_modifiers' =
- [Args.$$$ addN >> K (I, simp_add_local),
- Args.$$$ delN >> K (I, simp_del_local),
- Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
- Args.$$$ otherN >> K (I, I)];
+ [Args.$$$ addN -- colon >> K (I, simp_add_local),
+ Args.$$$ delN -- colon >> K (I, simp_del_local),
+ Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
+ Args.$$$ otherN -- colon >> K (I, I)];
fun simp_method tac =
(fn prems => fn ctxt => Method.METHOD (fn facts =>