# HG changeset patch
# User haftmann
# Date 1285680779 -7200
# Node ID d46cbac5bd827702aba492b6fd5f2538b4e5c4b8
# Parent  b4bd83468600de0ef31a53a4fe2eb9ead3ea2835
dropped syntax for old primrec package

diff -r b4bd83468600 -r d46cbac5bd82 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Sep 28 12:48:05 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Tue Sep 28 15:32:59 2010 +0200
@@ -320,12 +320,7 @@
 val _ =
   Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
   Keyword.thy_decl
-    ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
-      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
-    || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
-      Toplevel.theory (snd o
-        (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
-          alt_name (map Parse.triple_swap eqns) o
-        tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
+    (primrec_decl >> (fn ((opt_target, fixes), specs) =>
+      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)));
 
 end;