# HG changeset patch
# User paulson
# Date 875526352 -7200
# Node ID f92594f65af6e7d0421d8c55df658f425e7bcc66
# Parent  ed63c05d7992a640331606f3f322790c2054840c
Default simpset tactics now dereference "simpset"
only when given the proof state

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