diff -r 1fc86cec3bdf -r 5e8cef567042 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -318,31 +318,7 @@
 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
 val add_primrec_i = gen_primrec_i thy_note (thy_def false);
 val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
-fun gen_primrec note def alt_name specs =
-  gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
 
 end;
 
-
-(* see primrec.ML (* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_unchecked_name =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
-      P.name >> pair false) --| P.$$$ ")")) (false, "");
-
-val primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-
-val _ =
-  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
-      Toplevel.theory (snd o
-        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
-          (map P.triple_swap eqns))));
-
-end;*)
-
 end;