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