src/HOL/Tools/recfun_codegen.ML
changeset 29272 fb3ccf499df5
parent 28703 aef727ef30e5
child 30190 479806475f3c
equal deleted inserted replaced
29271:1d685baea08e 29272:fb3ccf499df5
     1 (*  Title:      HOL/Tools/recfun_codegen.ML
     1 (*  Title:      HOL/Tools/recfun_codegen.ML
     2     ID:         $Id$
       
     3     Author:     Stefan Berghofer, TU Muenchen
     2     Author:     Stefan Berghofer, TU Muenchen
     4 
     3 
     5 Code generator for recursive functions.
     4 Code generator for recursive functions.
     6 *)
     5 *)
     7 
     6 
    44 
    43 
    45 fun expand_eta thy [] = []
    44 fun expand_eta thy [] = []
    46   | expand_eta thy (thms as thm :: _) =
    45   | expand_eta thy (thms as thm :: _) =
    47       let
    46       let
    48         val (_, ty) = Code_Unit.const_typ_eqn thm;
    47         val (_, ty) = Code_Unit.const_typ_eqn thm;
    49       in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
    48       in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
    50         then thms
    49         then thms
    51         else map (Code_Unit.expand_eta thy 1) thms
    50         else map (Code_Unit.expand_eta thy 1) thms
    52       end;
    51       end;
    53 
    52 
    54 fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
    53 fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else