# HG changeset patch
# User paulson
# Date 842633305 -7200
# Node ID adb88d42f1bd4b401591ba1307992529d00923d0
# Parent  b5efc4108d045016d012c3dae980b70d8f0af6fe
Abstraction of enemy_analz_tac over its argument

diff -r b5efc4108d04 -r adb88d42f1bd src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Sep 13 18:47:01 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Sep 13 18:48:25 1996 +0200
@@ -12,6 +12,9 @@
 
 Addsimps [parts_cut_eq];
 
+(*GOALS.ML??*)
+fun prlim n = (goals_limit:=n; pr());
+
 (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
 by (fast_tac (!claset addEs [equalityE]) 1);
@@ -224,8 +227,9 @@
     match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
     ORELSE' etac FalseE;
 
-(*Analysis of Fake cases and of messages that forward unknown parts*)
-val enemy_analz_tac =
+(*Analysis of Fake cases and of messages that forward unknown parts
+  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
+fun enemy_analz_tac i =
   SELECT_GOAL 
    (EVERY [  (*push in occurrences of X...*)
 	   (REPEAT o CHANGED)
@@ -238,6 +242,6 @@
 	   Fast_tac 1,
 	   Asm_full_simp_tac 1,
 	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
-	   ]);
+	   ]) i;