1.1 --- a/src/Tools/Code/code_preproc.ML	Wed Dec 02 17:53:35 2009 +0100
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Dec 02 17:53:35 2009 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4        -- perhaps by means of upcoming code certificates with a corresponding
     1.5           preprocessor protocol*);
     1.6  
     1.7 -fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
     1.8 +fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
     1.9  
    1.10  fun eqn_conv conv =
    1.11    let
    1.12 @@ -148,7 +148,7 @@
    1.13    in
    1.14      ct
    1.15      |> Simplifier.rewrite pre
    1.16 -    |> rhs_conv (AxClass.unoverload_conv thy)
    1.17 +    |> trans_conv_rule (AxClass.unoverload_conv thy)
    1.18    end;
    1.19  
    1.20  fun postprocess_conv thy ct =
    1.21 @@ -157,7 +157,7 @@
    1.22    in
    1.23      ct
    1.24      |> AxClass.overload_conv thy
    1.25 -    |> rhs_conv (Simplifier.rewrite post)
    1.26 +    |> trans_conv_rule (Simplifier.rewrite post)
    1.27    end;
    1.28  
    1.29  fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);