diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Thu May 10 00:39:46 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Thu May 10 00:39:48 2007 +0200
@@ -314,18 +314,18 @@
       fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
     fun rhs_conv conv thm =
       let
-        val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
+        val thm' = (conv o Thm.rhs_of) thm;
       in Thm.transitive thm thm' end
     val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
     val thm1 = CodegenData.preprocess_cterm ct
       |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
-    val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
+    val ct' = Thm.rhs_of thm1;
     val consts = consts_of thy (Thm.term_of ct');
     val funcgr' = ensure_consts rewrites thy consts funcgr;
     val algebra = CodegenData.coregular_algebra thy;
     val (_, thm2) = Thm.varifyT' [] thm1;
-    val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
+    val thm3 = Thm.reflexive (Thm.rhs_of thm2);
     val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy);
     val [thm4] = resort_thms algebra typ_funcgr [thm3];
     val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
@@ -337,7 +337,7 @@
       in Thm.instantiate (instmap, []) thm end;
     val thm5 = inst thm2;
     val thm6 = inst thm4;
-    val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6);
+    val ct'' = Thm.rhs_of thm6;
     val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
     val drop = drop_classes thy tfrees;
     val instdefs = instances_of_consts thy algebra funcgr' cs;