src/HOL/Tools/recfun_codegen.ML
changeset 15700 970e0293dfb3
parent 15574 b1d1b5bfc464
child 16424 18a07ad8fea8
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Apr 12 11:08:25 2005 +0200
@@ -29,7 +29,6 @@
 
 structure CodegenData = TheoryDataFun(CodegenArgs);
 
-val prop_of = #prop o rep_thm;
 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
 val lhs_of = fst o dest_eqn o prop_of;
 val const_of = dest_Const o head_of o fst o dest_eqn;