src/HOL/W0/W.ML

 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
                             free_tv_app_subst_te RS subsetD,
                             free_tv_app_subst_tel RS subsetD,
                             less_le_trans,subsetD]
                      addSEs [UnE]
-                     addss simpset()) 1); 
+                     addss (simpset() setSolver unsafe_solver)) 1);
+(* builtin arithmetic in simpset messes things up *)
 qed_spec_mp "free_tv_W"; 
 
 (* Completeness of W w.r.t. has_type *)
 Goal "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
 \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \