src/HOL/Tools/old_primrec.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4            let
     1.5              val (f, ts) = strip_comb t;
     1.6            in
     1.7 -            if is_Const f andalso dest_Const f mem map fst rec_eqns then
     1.8 +            if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
     1.9                let
    1.10                  val fnameT' as (fname', _) = dest_Const f;
    1.11                  val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');