--- a/src/HOL/Tools/recfun_codegen.ML Tue Jun 06 14:56:42 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Jun 06 14:57:13 2006 +0200
@@ -9,7 +9,6 @@
sig
val add: string option -> attribute
val del: attribute
- val get_thm_equations: theory -> string * typ -> (thm list * typ) option
val setup: theory -> theory
end;
@@ -86,17 +85,6 @@
| SOME thyname => thyname)
end);
-fun get_thm_equations thy (c, ty) =
- Symtab.lookup (CodegenData.get thy) c
- |> Option.map (fn thms =>
- List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms
- |> del_redundant thy [])
- |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
- |> Option.map (fn thms =>
- (preprocess thy (map fst thms),
- (snd o const_of o prop_of o fst o hd) thms))
- |> (Option.map o apfst o map) (fn thm => thm RS HOL.eq_reflection);
-
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");