src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/simpdata.ML	Sun Feb 28 22:30:51 2010 +0100
@@ -32,9 +32,9 @@
 (*Analyse a rigid formula*)
 val ZF_conn_pairs =
   [("Ball",     [@{thm bspec}]),
-   ("All",      [spec]),
-   ("op -->",   [mp]),
-   ("op &",     [conjunct1,conjunct2])];
+   ("All",      [@{thm spec}]),
+   ("op -->",   [@{thm mp}]),
+   ("op &",     [@{thm conjunct1}, @{thm conjunct2}])];
 
 (*Analyse a:b, where b is rigid*)
 val ZF_mem_pairs =