src/HOL/TLA/Stfun.ML

--- a/src/HOL/TLA/Stfun.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/TLA/Stfun.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -20,6 +20,6 @@
 qed_goal "PairVarE" Stfun.thy
   "[| <v,w> u = (x,y); [| v u = x; w u = y |] ==> PROP R |] ==> PROP R"
   (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
-		ALLGOALS (asm_full_simp_tac (!simpset addsimps [pairSF_def]))
+		ALLGOALS (asm_full_simp_tac (simpset() addsimps [pairSF_def]))
                ]);