# HG changeset patch
# User wenzelm
# Date 1392071084 -3600
# Node ID bc34c5774f26d4663be7c317b2c51498a5ea8de4
# Parent  d44b415ae99e94af7bad2a1ad99b5f911faff4b4# Parent  51f0876f61dfcdceb04b5af1cb9e00fa89e4a46a
merged

diff -r d44b415ae99e -r bc34c5774f26 NEWS
--- a/NEWS	Mon Feb 10 21:51:15 2014 +0100
+++ b/NEWS	Mon Feb 10 23:24:44 2014 +0100
@@ -44,6 +44,16 @@
 
 *** Pure ***
 
+* Low-level type-class commands 'classes', 'classrel', 'arities' have
+been discontinued to avoid the danger of non-trivial axiomatization
+that is not immediately visible.  INCOMPATIBILITY, use regular
+'instance' with proof.  The required OFCLASS(...) theorem might be
+postulated via 'axiomatization' beforehand, or the proof finished
+trivially if the underlying class definition is made vacuous (without
+any assumptions).  See also Isabelle/ML operations
+Axclass.axiomatize_class, Axclass.axiomatize_classrel,
+Axclass.axiomatize_arity.
+
 * Attributes "where" and "of" allow an optional context of local
 variables ('for' declaration): these variables become schematic in the
 instantiated theorem.
diff -r d44b415ae99e -r bc34c5774f26 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Feb 10 21:51:15 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Feb 10 23:24:44 2014 +0100
@@ -24,7 +24,6 @@
     "also"
     "apply"
     "apply_end"
-    "arities"
     "assume"
     "attribute_setup"
     "axiomatization"
@@ -37,8 +36,6 @@
     "chapter"
     "class"
     "class_deps"
-    "classes"
-    "classrel"
     "codatatype"
     "code_datatype"
     "coinductive"
@@ -346,13 +343,10 @@
   '("ML"
     "ML_file"
     "abbreviation"
-    "arities"
     "attribute_setup"
     "axiomatization"
     "bundle"
     "class"
-    "classes"
-    "classrel"
     "codatatype"
     "code_datatype"
     "coinductive"
diff -r d44b415ae99e -r bc34c5774f26 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Feb 10 21:51:15 2014 +0100
+++ b/etc/isar-keywords.el	Mon Feb 10 23:24:44 2014 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-FP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -25,7 +25,6 @@
     "also"
     "apply"
     "apply_end"
-    "arities"
     "assume"
     "atom_decl"
     "attribute_setup"
@@ -45,24 +44,16 @@
     "chapter"
     "class"
     "class_deps"
-    "classes"
-    "classrel"
     "codatatype"
-    "code_class"
-    "code_const"
     "code_datatype"
     "code_deps"
     "code_identifier"
-    "code_include"
-    "code_instance"
-    "code_modulename"
     "code_monad"
     "code_pred"
     "code_printing"
     "code_reflect"
     "code_reserved"
     "code_thms"
-    "code_type"
     "coinductive"
     "coinductive_set"
     "commit"
@@ -487,7 +478,6 @@
     "ML_file"
     "abbreviation"
     "adhoc_overloading"
-    "arities"
     "atom_decl"
     "attribute_setup"
     "axiomatization"
@@ -496,21 +486,13 @@
     "bundle"
     "case_of_simps"
     "class"
-    "classes"
-    "classrel"
     "codatatype"
-    "code_class"
-    "code_const"
     "code_datatype"
     "code_identifier"
-    "code_include"
-    "code_instance"
-    "code_modulename"
     "code_monad"
     "code_printing"
     "code_reflect"
     "code_reserved"
-    "code_type"
     "coinductive"
     "coinductive_set"
     "consts"
diff -r d44b415ae99e -r bc34c5774f26 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/CCL/CCL.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/CCL/Set.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/Classes/Classes.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -356,19 +356,14 @@
 consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
 
 text {*
-  \noindent The connection to the type system is done by means
-  of a primitive type class
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-classes %quote idem < type
-(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
-setup %invisible {* Sign.parent_path *}(*>*)
-
-text {* \noindent together with a corresponding interpretation: *}
+  \noindent The connection to the type system is done by means of a
+  primitive type class @{text "idem"}, together with a corresponding
+  interpretation:
+*}
 
 interpretation %quote idem_class:
   idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-(*<*)proof qed (rule idem)(*>*)
+(*<*)sorry(*>*)
 
 text {*
   \noindent This gives you the full power of the Isabelle module system;
diff -r d44b415ae99e -r bc34c5774f26 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -1085,36 +1085,19 @@
 
 section {* Primitive specification elements *}
 
-subsection {* Type classes and sorts \label{sec:classes} *}
+subsection {* Sorts *}
 
 text {*
   \begin{matharray}{rcll}
-    @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
   \end{matharray}
 
   @{rail \<open>
-    @@{command classes} (@{syntax classdecl} +)
-    ;
-    @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
-    ;
     @@{command default_sort} @{syntax sort}
   \<close>}
 
   \begin{description}
 
-  \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
-  @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
-  Isabelle implicitly maintains the transitive closure of the class
-  hierarchy.  Cyclic class structures are not permitted.
-
-  \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
-  relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
-  This is done axiomatically!  The @{command_ref "subclass"} and
-  @{command_ref "instance"} commands (see \secref{sec:class}) provide
-  a way to introduce proven class relations.
-
   \item @{command "default_sort"}~@{text s} makes sort @{text s} the
   new default sort for any type variable that is given explicitly in
   the text, but lacks a sort constraint (wrt.\ the current context).
@@ -1138,15 +1121,12 @@
   \begin{matharray}{rcll}
     @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
   @{rail \<open>
     @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
     ;
     @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
-    ;
-    @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
   \<close>}
 
   \begin{description}
@@ -1161,14 +1141,7 @@
   \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
   type constructor @{text t}.  If the object-logic defines a base sort
   @{text s}, then the constructor is declared to operate on that, via
-  the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
-  s)s"}.
-
-  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
-  Isabelle's order-sorted signature of types by new type constructor
-  arities.  This is done axiomatically!  The @{command_ref "instantiation"}
-  target (see \secref{sec:class}) provides a way to introduce
-  proven type arities.
+  the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
 
   \end{description}
 *}
diff -r d44b415ae99e -r bc34c5774f26 src/Doc/ROOT
--- a/src/Doc/ROOT	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/ROOT	Mon Feb 10 23:24:44 2014 +0100
@@ -1,7 +1,7 @@
 chapter Doc
 
 session Classes (doc) in "Classes" = HOL +
-  options [document_variants = "classes"]
+  options [document_variants = "classes", quick_and_dirty]
   theories [document = false] Setup
   theories Classes
   files
diff -r d44b415ae99e -r bc34c5774f26 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/IFOL.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -24,7 +24,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-classes "term"
+class "term"
 default_sort "term"
 
 typedecl o
diff -r d44b415ae99e -r bc34c5774f26 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Nat.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat  ("0") and
diff -r d44b415ae99e -r bc34c5774f26 src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -14,7 +14,7 @@
 *}
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat    ("0") and
diff -r d44b415ae99e -r bc34c5774f26 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Prolog.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -13,7 +13,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-classes "term"
+class "term"
 default_sort "term"
 
 typedecl p
diff -r d44b415ae99e -r bc34c5774f26 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOLP/ex/Nat.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat    ("0") and
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -45,13 +45,15 @@
 
 subsubsection {* Core syntax *}
 
-classes type
+setup {* Axclass.axiomatize_class (@{binding type}, []) *}
 default_sort type
 setup {* Object_Logic.add_base_sort @{sort type} *}
 
-arities
-  "fun" :: (type, type) type
-  itself :: (type) type
+axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
+instance "fun" :: (type, type) type by (rule fun_arity)
+
+axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
+instance itself :: (type) type by (rule itself_arity)
 
 typedecl bool
 
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/HOLCF/ex/Focus_ex.thy
--- a/src/HOL/HOLCF/ex/Focus_ex.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -103,7 +103,8 @@
 begin
 
 typedecl ('a, 'b) tc
-arities tc:: (pcpo, pcpo) pcpo
+axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)"
+instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
 
 axiomatization
   Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -632,82 +632,4 @@
 
 ML_file "distinct_tree_prover.ML"
 
-(* Uncomment for profiling or debugging *)
-(*
-ML {*
-(*
-val nums = (0 upto 10000);
-val nums' = (200 upto 3000);
-*)
-val nums = (0 upto 10000);
-val nums' = (0 upto 3000);
-val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
-
-val consts = sort Term_Ord.fast_term_ord 
-              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term_Ord.fast_term_ord 
-              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
-
-val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
-
-
-val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
-
-
-val dist = 
-     HOLogic.Trueprop$
-       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
-
-val dist' = 
-     HOLogic.Trueprop$
-       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
-
-val da = Unsynchronized.ref refl;
-
-*}
-
-setup {*
-Theory.add_consts_i const_decls
-#> (fn thy  => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
-               in (da := thm; thy') end)
-*}
-
-
-ML {* 
- val ct' = cterm_of @{theory} t';
-*}
-
-ML {*
- timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
-*}
-
-(* 590 s *)
-
-ML {*
-
-
-val p1 = 
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
-val p2 =
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
-*}
-
-
-ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
-       p1
-       p2)*}
-
-
-ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
-
-
-
-
-ML {*
-val cdist' = cterm_of @{theory} dist';
-DistinctTreeProver.distinct_implProver (!da) cdist';
-*}
-
-*)
-
 end
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Action.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -15,7 +15,7 @@
 type_synonym 'a trfun = "(state * state) => 'a"
 type_synonym action   = "bool trfun"
 
-arities prod :: (world, world) world
+instance prod :: (world, world) world ..
 
 consts
   (** abstract syntax **)
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Init.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -12,7 +12,7 @@
 begin
 
 typedecl behavior
-arities behavior :: world
+instance behavior :: world ..
 
 type_synonym temporal = "behavior form"
 
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -10,8 +10,7 @@
 imports Main
 begin
 
-classes world
-classrel world < type
+class world
 
 (** abstract syntax **)
 
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Stfun.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -10,8 +10,7 @@
 begin
 
 typedecl state
-
-arities state :: world
+instance state :: world ..
 
 type_synonym 'a stfun = "state => 'a"
 type_synonym stpred  = "bool stfun"
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -285,7 +285,7 @@
         |> Sign.add_consts_i
           (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
            dst_preds)
-        |> fold_map Specification.axiom
+        |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
             (map_index (fn (j, (predname, t)) =>
                 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
               (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -118,8 +118,9 @@
           val new_defs = map mk_def srs
           val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> fold_map Specification.axiom (map_index
-              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
+          |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
+            (map_index (fn (i, t) =>
+              ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
         in
           (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end
diff -r d44b415ae99e -r bc34c5774f26 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/LCF/LCF.thy	Mon Feb 10 23:24:44 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 d44b415ae99e -r bc34c5774f26 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/General/output.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -25,19 +25,6 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
-  structure Internal:
-  sig
-    val writeln_fn: (output -> unit) Unsynchronized.ref
-    val urgent_message_fn: (output -> unit) Unsynchronized.ref
-    val tracing_fn: (output -> unit) Unsynchronized.ref
-    val warning_fn: (output -> unit) Unsynchronized.ref
-    val error_message_fn: (serial * output -> unit) Unsynchronized.ref
-    val prompt_fn: (output -> unit) Unsynchronized.ref
-    val status_fn: (output -> unit) Unsynchronized.ref
-    val report_fn: (output -> unit) Unsynchronized.ref
-    val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
-    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
-  end
   val urgent_message: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
@@ -49,7 +36,22 @@
   val try_protocol_message: Properties.T -> string -> unit
 end;
 
-structure Output: OUTPUT =
+signature PRIVATE_OUTPUT =
+sig
+  include OUTPUT
+  val writeln_fn: (output -> unit) Unsynchronized.ref
+  val urgent_message_fn: (output -> unit) Unsynchronized.ref
+  val tracing_fn: (output -> unit) Unsynchronized.ref
+  val warning_fn: (output -> unit) Unsynchronized.ref
+  val error_message_fn: (serial * output -> unit) Unsynchronized.ref
+  val prompt_fn: (output -> unit) Unsynchronized.ref
+  val status_fn: (output -> unit) Unsynchronized.ref
+  val report_fn: (output -> unit) Unsynchronized.ref
+  val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+end;
+
+structure Output: PRIVATE_OUTPUT =
 struct
 
 (** print modes **)
@@ -92,33 +94,30 @@
 
 exception Protocol_Message of Properties.T;
 
-structure Internal =
-struct
-  val writeln_fn = Unsynchronized.ref physical_writeln;
-  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
-  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
-  val error_message_fn =
-    Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
-  val prompt_fn = Unsynchronized.ref physical_stdout;
-  val status_fn = Unsynchronized.ref (fn _: output => ());
-  val report_fn = Unsynchronized.ref (fn _: output => ());
-  val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
-  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-end;
+val writeln_fn = Unsynchronized.ref physical_writeln;
+val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
+val error_message_fn =
+  Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
+val prompt_fn = Unsynchronized.ref physical_stdout;
+val status_fn = Unsynchronized.ref (fn _: output => ());
+val report_fn = Unsynchronized.ref (fn _: output => ());
+val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
+val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 
-fun writeln s = ! Internal.writeln_fn (output s);
-fun urgent_message s = ! Internal.urgent_message_fn (output s);  (*Proof General legacy*)
-fun tracing s = ! Internal.tracing_fn (output s);
-fun warning s = ! Internal.warning_fn (output s);
-fun error_message' (i, s) = ! Internal.error_message_fn (i, output s);
+fun writeln s = ! writeln_fn (output s);
+fun urgent_message s = ! urgent_message_fn (output s);  (*Proof General legacy*)
+fun tracing s = ! tracing_fn (output s);
+fun warning s = ! warning_fn (output s);
+fun error_message' (i, s) = ! error_message_fn (i, output s);
 fun error_message s = error_message' (serial (), s);
-fun prompt s = ! Internal.prompt_fn (output s);
-fun status s = ! Internal.status_fn (output s);
-fun report s = ! Internal.report_fn (output s);
-fun result props s = ! Internal.result_fn props (output s);
-fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
+fun prompt s = ! prompt_fn (output s);
+fun status s = ! status_fn (output s);
+fun report s = ! report_fn (output s);
+fun result props s = ! result_fn props (output s);
+fun protocol_message props s = ! protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 
 end;
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -73,19 +73,7 @@
 
 (** theory commands **)
 
-(* classes and sorts *)
-
-val _ =
-  Outer_Syntax.command @{command_spec "classes"} "declare type classes"
-    (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
-        Parse.!!! (Parse.list1 Parse.class)) [])
-      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
-    (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
-        |-- Parse.!!! Parse.class))
-    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
+(* sorts *)
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "default_sort"}
@@ -111,10 +99,6 @@
     "declare syntactic type constructors (grammar nonterminal symbols)"
     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
-val _ =
-  Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
-    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
-
 
 (* consts and syntax *)
 
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Pure.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -25,10 +25,9 @@
   and "subsect" :: prf_heading3 % "proof"
   and "subsubsect" :: prf_heading4 % "proof"
   and "txt" "txt_raw" :: prf_decl % "proof"
-  and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
-    "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
-    "translations" "no_translations" "defs" "definition"
-    "abbreviation" "type_notation" "no_type_notation" "notation"
+  and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment"
+    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
+    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   and "ML" :: thy_decl % "ML"
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/ROOT.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -306,6 +306,8 @@
 use "Tools/named_thms.ML";
 use "Tools/proof_general.ML";
 
+structure Output: OUTPUT = Output;  (*seal system channels!*)
+
 
 (* ML toplevel pretty printing *)
 
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -111,19 +111,19 @@
         message name
           (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
   in
-    Output.Internal.status_fn := standard_message [] Markup.statusN;
-    Output.Internal.report_fn := standard_message [] Markup.reportN;
-    Output.Internal.result_fn :=
+    Output.status_fn := standard_message [] Markup.statusN;
+    Output.report_fn := standard_message [] Markup.reportN;
+    Output.result_fn :=
       (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
-    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
-    Output.Internal.tracing_fn :=
+    Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
+    Output.tracing_fn :=
       (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
-    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
-    Output.Internal.error_message_fn :=
+    Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+    Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
-    Output.Internal.protocol_message_fn := message Markup.protocolN;
-    Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
-    Output.Internal.prompt_fn := ignore;
+    Output.protocol_message_fn := message Markup.protocolN;
+    Output.urgent_message_fn := ! Output.writeln_fn;
+    Output.prompt_fn := ignore;
     message Markup.initN [] (Session.welcome ());
     msg_channel
   end;
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/isar.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -157,7 +157,7 @@
  (Context.set_thread_data NONE;
   Multithreading.max_threads_update (Options.default_int "threads");
   if do_init then init () else ();
-  Output.Internal.protocol_message_fn := protocol_message;
+  Output.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/session.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -57,6 +57,7 @@
   Outer_Syntax.check_syntax ();
   Future.shutdown ();
   Event_Timer.shutdown ();
+  Future.shutdown ();
   session_finished := true);
 
 
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Tools/build.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -166,7 +166,7 @@
         theories |>
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
-            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
+            |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
             |> Multithreading.max_threads_setmp (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Tools/proof_general.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -264,14 +264,14 @@
   | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (Output.Internal.writeln_fn := message "" "" "";
-  Output.Internal.status_fn := (fn _ => ());
-  Output.Internal.report_fn := (fn _ => ());
-  Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
-  Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.Internal.warning_fn := message (special "K") (special "L") "### ";
-  Output.Internal.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (Output.writeln_fn := message "" "" "";
+  Output.status_fn := (fn _ => ());
+  Output.report_fn := (fn _ => ());
+  Output.urgent_message_fn := message (special "I") (special "J") "";
+  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.warning_fn := message (special "K") (special "L") "### ";
+  Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+  Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 
 (* notification *)
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/axclass.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -30,12 +30,9 @@
   val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
   val define_class: binding * class list -> string list ->
     (Thm.binding * term list) list -> theory -> class * theory
+  val axiomatize_classrel: (class * class) list -> theory -> theory
+  val axiomatize_arity: arity -> theory -> theory
   val axiomatize_class: binding * class list -> theory -> theory
-  val axiomatize_class_cmd: binding * xstring list -> theory -> theory
-  val axiomatize_classrel: (class * class) list -> theory -> theory
-  val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
-  val axiomatize_arity: arity -> theory -> theory
-  val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
 end;
 
 structure Axclass: AXCLASS =
@@ -596,38 +593,30 @@
     |-> fold (add o Drule.export_without_context o snd)
   end;
 
-fun ax_classrel prep =
-  axiomatize (map o prep) (map Logic.mk_classrel)
-    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
-
-fun ax_arity prep =
-  axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
-    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
-
 fun class_const c =
   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
 
-fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
+in
+
+val axiomatize_classrel =
+  axiomatize (map o cert_classrel) (map Logic.mk_classrel)
+    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
+
+val axiomatize_arity =
+  axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
+    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
+
+fun axiomatize_class (bclass, raw_super) thy =
   let
     val class = Sign.full_name thy bclass;
-    val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
+    val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
   in
     thy
     |> Sign.primitive_class (bclass, super)
-    |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
+    |> axiomatize_classrel (map (fn c => (class, c)) super)
     |> Theory.add_deps_global "" (class_const class) (map class_const super)
   end;
 
-in
-
-val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd =
-  ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
-val axiomatize_classrel = ax_classrel cert_classrel;
-val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity Proof_Context.cert_arity;
-val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
-
 end;
 
 end;
diff -r d44b415ae99e -r bc34c5774f26 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Mon Feb 10 23:24:44 2014 +0100
@@ -375,11 +375,7 @@
 
 fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
 
-fun put_simpset ss = map_simpset (fn context_ss =>
-  let
-    val Simpset ({rules, prems, ...}, ss2) = ss;  (* FIXME prems from context (!?) *)
-    val Simpset ({depth, ...}, _) = context_ss;
-  in Simpset (make_ss1 (rules, prems, depth), ss2) end);
+fun put_simpset ss = map_simpset (K ss);
 
 val empty_simpset = put_simpset empty_ss;
 
diff -r d44b415ae99e -r bc34c5774f26 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Sequents/LK/Nat.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
 begin
 
 typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
 
 axiomatization
   Zero :: nat      ("0") and
diff -r d44b415ae99e -r bc34c5774f26 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Sequents/LK0.thy	Mon Feb 10 23:24:44 2014 +0100
@@ -12,7 +12,7 @@
 imports Sequents
 begin
 
-classes "term"
+class "term"
 default_sort "term"
 
 consts
diff -r d44b415ae99e -r bc34c5774f26 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Feb 10 21:51:15 2014 +0100
+++ b/src/ZF/ZF.thy	Mon Feb 10 23:24:44 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