src/Pure/Isar/class_declaration.ML

--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -97,7 +97,7 @@
     fun tac ctxt =
       REPEAT (SOMEGOAL
         (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
-          ORELSE' assume_tac));
+          ORELSE' assume_tac ctxt));
     val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
 
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;