# HG changeset patch
# User wenzelm
# Date 1392049211 -3600
# Node ID 4de48353034e9892c1a03079d7cc3ce1614465f9
# Parent  9701dbc35f867ba2ecbc49bd44758d5d1800f22a
prefer vacuous definitional type classes over axiomatic ones;

diff -r 9701dbc35f86 -r 4de48353034e src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/CCL/CCL.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -16,13 +16,13 @@
   being defined which contains only executable terms.
 *}
 
-classes prog < "term"
+class prog = "term"
 default_sort prog
 
-arities "fun" :: (prog, prog) prog
+instance "fun" :: (prog, prog) prog ..
 
 typedecl i
-arities i :: prog
+instance i :: prog ..
 
 
 consts
diff -r 9701dbc35f86 -r 4de48353034e src/CCL/Set.thy
--- a/src/CCL/Set.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/CCL/Set.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -7,7 +7,7 @@
 declare [[eta_contract]]
 
 typedecl 'a set
-arities set :: ("term") "term"
+instance set :: ("term") "term" ..
 
 consts
   Collect       :: "['a => o] => 'a set"                    (*comprehension*)
diff -r 9701dbc35f86 -r 4de48353034e src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOL/IFOL.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -24,7 +24,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-classes "term"
+class "term"
 default_sort "term"
 
 typedecl o
diff -r 9701dbc35f86 -r 4de48353034e src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -8,7 +8,9 @@
 imports FOL
 begin
 
-typedecl int arities int :: "term"
+typedecl int
+instance int :: "term" ..
+
 consts plus :: "int => int => int" (infixl "+" 60)
   zero :: int ("0")
   minus :: "int => int" ("- _")
diff -r 9701dbc35f86 -r 4de48353034e src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOL/ex/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat  ("0") and
diff -r 9701dbc35f86 -r 4de48353034e src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -14,7 +14,7 @@
 *}
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat    ("0") and
diff -r 9701dbc35f86 -r 4de48353034e src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOL/ex/Prolog.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl 'a list
-arities list :: ("term") "term"
+instance list :: ("term") "term" ..
 
 axiomatization
   Nil     :: "'a list" and
diff -r 9701dbc35f86 -r 4de48353034e src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -13,7 +13,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-classes "term"
+class "term"
 default_sort "term"
 
 typedecl p
diff -r 9701dbc35f86 -r 4de48353034e src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/FOLP/ex/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat    ("0") and
diff -r 9701dbc35f86 -r 4de48353034e src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -18,13 +18,12 @@
 
 subsection {* Pure Logic *}
 
-classes type
+class type
 default_sort type
 
 typedecl o
-arities
-  o :: type
-  "fun" :: (type, type) type
+instance o :: type ..
+instance "fun" :: (type, type) type ..
 
 
 subsubsection {* Basic logical connectives *}
diff -r 9701dbc35f86 -r 4de48353034e src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/LCF/LCF.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -13,7 +13,7 @@
 
 subsection {* Natural Deduction Rules for LCF *}
 
-classes cpo < "term"
+class cpo = "term"
 default_sort cpo
 
 typedecl tr
@@ -21,12 +21,11 @@
 typedecl ('a,'b) prod  (infixl "*" 6)
 typedecl ('a,'b) sum  (infixl "+" 5)
 
-arities
-  "fun" :: (cpo, cpo) cpo
-  prod :: (cpo, cpo) cpo
-  sum :: (cpo, cpo) cpo
-  tr :: cpo
-  void :: cpo
+instance "fun" :: (cpo, cpo) cpo ..
+instance prod :: (cpo, cpo) cpo ..
+instance sum :: (cpo, cpo) cpo ..
+instance tr :: cpo ..
+instance void :: cpo ..
 
 consts
  UU     :: "'a"
diff -r 9701dbc35f86 -r 4de48353034e src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/Sequents/LK/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat      ("0") and
diff -r 9701dbc35f86 -r 4de48353034e src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/Sequents/LK0.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -12,7 +12,7 @@
 imports Sequents
 begin
 
-classes "term"
+class "term"
 default_sort "term"
 
 consts
diff -r 9701dbc35f86 -r 4de48353034e src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/ZF/ZF.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -12,7 +12,7 @@
 declare [[eta_contract = false]]
 
 typedecl i
-arities  i :: "term"
+instance i :: "term" ..
 
 axiomatization
   zero :: "i"  ("0")   --{*the empty set*}  and