Default simpset tactics now dereference "simpset"
only when given the proof state

--- a/src/Provers/simplifier.ML	Mon Sep 29 11:44:56 1997 +0200
+++ b/src/Provers/simplifier.ML	Mon Sep 29 11:45:52 1997 +0200
@@ -282,10 +282,12 @@
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
 val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true);
 
-fun          Simp_tac i =          simp_tac (! simpset) i;
-fun      Asm_simp_tac i =      asm_simp_tac (! simpset) i;
-fun     Full_simp_tac i =     full_simp_tac (! simpset) i;
-fun Asm_full_simp_tac i = asm_full_simp_tac (! simpset) i;
+(** The abstraction over the proof state delays the dereferencing **)
+
+fun          Simp_tac i st =          simp_tac (! simpset) i st;
+fun      Asm_simp_tac i st =      asm_simp_tac (! simpset) i st;
+fun     Full_simp_tac i st =     full_simp_tac (! simpset) i st;
+fun Asm_full_simp_tac i st = asm_full_simp_tac (! simpset) i st;