# HG changeset patch
# User haftmann
# Date 1149598633 -7200
# Node ID be3a84d22a5849d21bd84fb09be4495a5b8ed1bf
# Parent  b949911ecff575425a37c2f2f574a00cb4b40d58
deleted legacy

diff -r b949911ecff5 -r be3a84d22a58 src/HOL/Tools/recfun_codegen.ML
--- 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 | _ => "");