src/HOL/Auth/Message.ML
changeset 2637 e9b203f854ae
parent 2559 06b6a499f8ae
child 2891 d8f254ad1ab9
--- 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'