diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -242,12 +242,12 @@
            delsimps @{thms atLeastLessThan_iff}) 1);
 
     val lthy' =
-      Class.prove_instantiation_instance (fn _ =>
-        Class.intro_classes_tac [] THEN
+      Class.prove_instantiation_instance (fn ctxt =>
+        Class.intro_classes_tac ctxt [] THEN
         rtac finite_UNIV 1 THEN
         rtac range_pos 1 THEN
-        simp_tac (put_simpset HOL_basic_ss lthy addsimps [def3]) 1 THEN
-        simp_tac (put_simpset HOL_basic_ss lthy addsimps [def2]) 1) lthy;
+        simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
+        simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;
 
     val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>
       let