# HG changeset patch
# User haftmann
# Date 1388524711 -3600
# Node ID 81b3194defe0c8339ce279b7a23be11e5edf8733
# Parent  dd04a8b654fc03b2f57174eba085edc12672b815
dropped unused material

diff -r dd04a8b654fc -r 81b3194defe0 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Dec 31 14:29:16 2013 +0100
+++ b/src/Pure/Isar/code.ML	Tue Dec 31 22:18:31 2013 +0100
@@ -27,14 +27,11 @@
   val const_typ_eqn: theory -> thm -> string * typ
   val expand_eta: theory -> int -> thm -> thm
   type cert
-  val empty_cert: theory -> string -> cert
-  val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
   val constrain_cert: theory -> sort list -> cert -> cert
   val conclude_cert: cert -> cert
   val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
   val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
     * (((term * string option) list * (term * string option)) * (thm option * bool)) list
-  val bare_thms_of_cert: theory -> cert -> thm list
   val pretty_cert: theory -> cert -> Pretty.T list
 
   (*executable code*)
@@ -864,13 +861,6 @@
   | pretty_cert thy (Abstract (abs_thm, _)) =
       [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
 
-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 (Projection _) = []
-  | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) =
-      [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))];
-
 end;