src/HOL/Tools/recfun_codegen.ML
changeset 17203 29b2563f5c11
parent 17144 6642e0f96f44
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Aug 31 15:46:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Aug 31 15:46:40 2005 +0200
     1.3 @@ -60,9 +60,8 @@
     1.4  fun del_redundant thy eqs [] = eqs
     1.5    | del_redundant thy eqs (eq :: eqs') =
     1.6      let
     1.7 -      val tsig = Sign.tsig_of (sign_of thy);
     1.8        val matches = curry
     1.9 -        (Pattern.matches tsig o pairself (lhs_of o fst))
    1.10 +        (Pattern.matches thy o pairself (lhs_of o fst))
    1.11      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    1.12  
    1.13  fun get_equations thy defs (s, T) =