src/HOL/Induct/Exp.ML

   using eval restricted to its functional part.  Note that the execution
   (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   functional on the argument (c,s).
 *)
-Goal
-    "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
-\         ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
+Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
+\     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
 by (etac exec.induct 1);
 by (ALLGOALS Full_simp_tac);
 by (Blast_tac 3);
 by (Blast_tac 1);
 by (rewtac Unique_def);