# HG changeset patch
# User haftmann
# Date 1267177701 -3600
# Node ID 212b1dc5212dde8eb40d81703f66b10eac0fd759
# Parent  cb06a11a7955176c16e8409449092149f591d21e
use abstract code cerficates for bare code theorems

diff -r cb06a11a7955 -r 212b1dc5212d 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;