# HG changeset patch
# User wenzelm
# Date 1435323834 -7200
# Node ID 479071e8778f54dff4bda63842e80a43267bc1ff
# Parent  b5622eef7176df34c3e18d7fac0f72c476baad1d
tuned proofs;

diff -r b5622eef7176 -r 479071e8778f src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 14:53:28 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 15:03:54 2015 +0200
@@ -61,7 +61,7 @@
   apply (rule equalityI)
    apply (rule subset_UNIV)
   apply (rule subsetI)
-  apply (drule_tac c = "(xa, arbitrary) " in basevars)
+  apply (drule_tac c = "(xa, _) " in basevars)
   apply auto
   done
 
@@ -70,7 +70,7 @@
   apply (rule equalityI)
    apply (rule subset_UNIV)
   apply (rule subsetI)
-  apply (drule_tac c = "(arbitrary, xa) " in basevars)
+  apply (drule_tac c = "(_, xa) " in basevars)
   apply auto
   done