--- a/src/HOL/TLA/Inc/Inc.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML Mon Nov 03 12:13:18 1997 +0100
@@ -10,7 +10,7 @@
val Psi_defs = [Psi_def,InitPsi_def,N1_def,N2_def,alpha1_def,alpha2_def,
beta1_def,beta2_def,gamma1_def,gamma2_def];
-val Inc_css = (!claset, !simpset);
+val Inc_css = (claset(), simpset());
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
@@ -55,7 +55,7 @@
More substantial examples require manual guidance anyway.
goal Inc.thy "Psi .-> []PsiInv";
-by (auto_inv_tac (!simpset addsimps PsiInv_defs @ Psi_defs @ pcount.simps) 1);
+by (auto_inv_tac (simpset() addsimps PsiInv_defs @ Psi_defs @ pcount.simps) 1);
*)