src/HOL/simpdata.ML
changeset 18176 ae9bd644d106
parent 17985 d5d576b72371
child 18324 d1c4b1112e33
     1.1 --- a/src/HOL/simpdata.ML	Wed Nov 16 15:29:23 2005 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Nov 16 17:45:22 2005 +0100
     1.3 @@ -204,7 +204,7 @@
     1.4                    let
     1.5                      val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
     1.6                    in SOME (rl OF [fx_g]) end 
     1.7 -               else if betapply (f,x) aconv g then NONE (* avoid identity conversion *)
     1.8 +               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
     1.9                 else let 
    1.10                       val abs_g'= Abs (n,xT,g');
    1.11                       val g'x = abs_g'$x;