--- a/src/Provers/simplifier.ML Fri Jul 21 17:46:34 2000 +0200
+++ b/src/Provers/simplifier.ML Fri Jul 21 17:46:38 2000 +0200
@@ -66,7 +66,6 @@
val full_simp_tac: simpset -> int -> tactic
val asm_lr_simp_tac: simpset -> int -> tactic
val asm_full_simp_tac: simpset -> int -> tactic
- val safe_asm_full_simp_tac: simpset -> int -> tactic
val Simp_tac: int -> tactic
val Asm_simp_tac: int -> tactic
val Full_simp_tac: int -> tactic
@@ -402,8 +401,6 @@
val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
-(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
-val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
(*the abstraction over the proof state delays the dereferencing*)
fun Simp_tac i st = simp_tac (simpset ()) i st;