# HG changeset patch
# User oheimb
# Date 964194398 -7200
# Node ID 7eb1753e802395da086f3d0325cdc657ee6cb936
# Parent  d3109d5173071950583a3bb755b88c4079912140
removed safe_asm_full_simp_tac

diff -r d3109d517307 -r 7eb1753e8023 src/Provers/simplifier.ML
--- 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;