src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Fri Feb 26 10:48:20 2010 +0100
+++ b/src/Pure/Isar/code.ML	Fri Feb 26 10:48:21 2010 +0100
@@ -840,7 +840,9 @@
 fun bare_thms_of_cert thy (cert as Equations _) =
       (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
         o snd o equations_of_cert thy) cert
-  | bare_thms_of_cert thy _ = [];
+  | bare_thms_of_cert thy (Projection _) = []
+  | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) =
+      [Thm.varifyT (snd (concretify_abs thy tyco abs_thm))];
 
 end;