1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val add: string option -> theory attribute
     1.5    val del: theory attribute
     1.6    val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
     1.7 +  val get_thm_equations: theory -> string * typ -> (thm list * typ) option
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -93,6 +94,17 @@
    1.12    |> apfst (map prop_of)
    1.13    |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
    1.14  
    1.15 +fun get_thm_equations thy (c, ty) =
    1.16 +  Symtab.lookup (CodegenData.get thy) c
    1.17 +  |> Option.map (fn thms => 
    1.18 +       List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms
    1.19 +       |> del_redundant thy [])
    1.20 +  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
    1.21 +  |> Option.map (fn thms =>
    1.22 +       (preprocess thy (map fst thms),
    1.23 +          (snd o const_of o prop_of o fst o hd) thms))
    1.24 +  |> (Option.map o apfst o map) (fn thm => thm RS HOL.eq_reflection);
    1.25 +
    1.26  fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    1.27    SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    1.28  
    1.29 @@ -185,8 +197,8 @@
    1.30    add_attribute ""
    1.31      (   Args.del |-- Scan.succeed del
    1.32       || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
    1.33 -  CodegenPackage.add_defgen
    1.34 -    ("rec", CodegenPackage.defgen_recfun get_rec_equations)
    1.35 +  CodegenPackage.add_eqextr
    1.36 +    ("rec", fn thy => fn _ => get_thm_equations thy)
    1.37  ];
    1.38  
    1.39  end;