--- a/src/HOL/Mutabelle/mutabelle.ML Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Sat Mar 15 11:59:18 2014 +0100
@@ -13,23 +13,11 @@
val mutate_sign : term -> theory -> (string * string) list -> int -> term list
val mutate_mix : term -> theory -> string list ->
(string * string) list -> int -> term list
-
- val all_unconcealed_thms_of : theory -> (string * thm) list
end;
structure Mutabelle : MUTABELLE =
struct
-fun all_unconcealed_thms_of thy =
- let
- val facts = Global_Theory.facts_of thy
- in
- Facts.fold_static
- (fn (s, ths) =>
- if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
- facts []
- end;
-
fun consts_of thy =
let
val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)