--- a/src/HOL/Auth/Message.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Message.ML Sat Feb 15 17:52:31 1997 +0100
@@ -825,13 +825,6 @@
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
val pushes = pushKeys@pushCrypts;
-
-(*No premature instantiation of variables during simplification.
- For proving "possibility" properties.*)
-fun safe_solver prems =
- match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
- ORELSE' etac FalseE;
-
val Fake_insert_tac =
dresolve_tac [impOfSubs Fake_analz_insert,
impOfSubs Fake_parts_insert] THEN'