# HG changeset patch
# User wenzelm
# Date 966614770 -7200
# Node ID ea1f02d6d65b9ca66ad1c92af8113102e0dcdb7e
# Parent  f0cfddda603873ca02b3d422f7a166f3d7d12ebc
removed obsolete add_recdef_x;

diff -r f0cfddda6038 -r ea1f02d6d65b src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Aug 18 17:58:33 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Aug 18 18:06:10 2000 +0200
@@ -104,7 +104,6 @@
   in (thy, result) end;
 
 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
-val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
 
 
@@ -147,7 +146,7 @@
 val recdef_decl =
   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
-  >> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs);
+  >> (fn (((f, R), eqs), congs) => #1 o add_recdef f R (map P.triple_swap eqs) None congs);
 
 val recdefP =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl