src/Provers/clasimp.ML

--- a/src/Provers/clasimp.ML	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/Provers/clasimp.ML	Sat Nov 17 17:55:52 2012 +0100
@@ -44,9 +44,6 @@
 
 (* simp as classical wrapper *)
 
-(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
-val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
-
 fun clasimp f name tac ctxt =
   Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;