src/HOL/Tools/Function/termination.ML
changeset 59625 aacdce52b2fc
parent 59621 291934bac95e
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 18:21:32 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 20:08:45 2015 +0100
     1.3 @@ -331,7 +331,7 @@
     1.4     val is = map (fn c => find_index (curry op aconv c) cs') cs
     1.5   in
     1.6     CONVERSION (Conv.arg_conv (Conv.arg_conv
     1.7 -     (Function_Lib.regroup_union_conv is))) i
     1.8 +     (Function_Lib.regroup_union_conv ctxt is))) i
     1.9   end)
    1.10  
    1.11