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