# HG changeset patch
# User haftmann
# Date 1285680887 -7200
# Node ID e4c85d8c2aba1a1ba4ee1ea88815a9e99c492a8f
# Parent  5d5fd2baf99dadbf311f23bd87291643086ee155# Parent  30cf9d80939e66f2bc04956493f2516ccb5c4010
merged

diff -r 30cf9d80939e -r e4c85d8c2aba NEWS
--- a/NEWS	Tue Sep 28 15:21:45 2010 +0200
+++ b/NEWS	Tue Sep 28 15:34:47 2010 +0200
@@ -74,10 +74,12 @@
 
 *** HOL ***
 
+* Dropped old primrec package.  INCOMPATIBILITY.
+
 * Improved infrastructure for term evaluation using code generator
 techniques, in particular static evaluation conversions.
 
-* String.literal is a type, but not a datatype. INCOMPATIBILITY.
+* String.literal is a type, but not a datatype.  INCOMPATIBILITY.
  
 * Renamed lemmas:
   expand_fun_eq -> fun_eq_iff
diff -r 30cf9d80939e -r e4c85d8c2aba src/HOL/SET_Protocol/SET_Protocol.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET_Protocol/SET_Protocol.thy	Tue Sep 28 15:34:47 2010 +0200
@@ -0,0 +1,12 @@
+(*  Title:      HOL/SET_Protocol/SET_Protocol.thy
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2003  University of Cambridge
+
+Root file for the SET protocol proofs.
+*)
+
+theory SET_Protocol
+imports Cardholder_Registration Merchant_Registration Purchase
+begin
+
+end
diff -r 30cf9d80939e -r e4c85d8c2aba src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Sep 28 15:21:45 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Tue Sep 28 15:34:47 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;