# HG changeset patch
# User blanchet
# Date 1410458386 -7200
# Node ID 18e6cb6a52977acbde6fcbb75a7dcc131fde1746
# Parent  6d8458bc6e27987229d8ebf6a9ca75da2f70e128
more porting to new datatypes

diff -r 6d8458bc6e27 -r 18e6cb6a5297 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Sep 11 19:45:42 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Sep 11 19:59:46 2014 +0200
@@ -81,7 +81,7 @@
   the formal text.  Examples may be seen in Isabelle/HOL sources
   itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
   @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
-  "\"old_datatype\""} @{text ":: thy_decl"} for theory-level declarations
+  "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
   with and without proof, respectively.  Additional @{syntax tags}
   provide defaults for document preparation (\secref{sec:tags}).
 
diff -r 6d8458bc6e27 -r 18e6cb6a5297 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Thu Sep 11 19:45:42 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Thu Sep 11 19:59:46 2014 +0200
@@ -37,7 +37,7 @@
 and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
   n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
 
-old_datatype 'a up = bot | Up 'a
+datatype 'a up = bot | Up 'a
 
 instantiation up :: (SL_top)SL_top
 begin