src/HOL/Tools/recfun_codegen.ML
changeset 38864 4abe644fcea5
parent 36692 54b64d4ad524
child 40844 5895c525739d
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4        end
     1.5    | avoid_value thy thms = thms;
     1.6  
     1.7 -fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
     1.8 +fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
     1.9    let
    1.10      val c = AxClass.unoverload_const thy (raw_c, T);
    1.11      val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c