instance command as rudimentary class target
authorhaftmann
Thu Nov 29 17:08:26 2007 +0100 (2007-11-29)
changeset 255029200b36280c0
parent 25501 845883bd3a6b
child 25503 fe14c6857f1d
instance command as rudimentary class target
NEWS
src/HOL/Complex/Complex.thy
src/HOL/Finite_Set.thy
src/HOL/IntDef.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Eval.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Product_ord.thy
src/HOL/List.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Nat.thy
src/HOL/Numeral.thy
src/HOL/Orderings.thy
src/HOL/Real/PReal.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/size.ML
src/HOL/ex/Classpackage.thy
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Thu Nov 29 07:55:46 2007 +0100
     1.2 +++ b/NEWS	Thu Nov 29 17:08:26 2007 +0100
     1.3 @@ -4,6 +4,14 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Command "instance" now takes list of definitions in the same
    1.10 +manner as the "definition" command.  Most notably, object equality is now
    1.11 +possible.  Type inference is more canonical than it used to be.
    1.12 +INCOMPATIBILITY: in some cases explicit type annotations are required.
    1.13 +
    1.14 +
    1.15  *** HOL ***
    1.16  
    1.17  * Constant "card" now with authentic syntax.
     2.1 --- a/src/HOL/Complex/Complex.thy	Thu Nov 29 07:55:46 2007 +0100
     2.2 +++ b/src/HOL/Complex/Complex.thy	Thu Nov 29 17:08:26 2007 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4    complex_minus_def:
     2.5      "- x \<equiv> Complex (- Re x) (- Im x)"
     2.6    complex_diff_def:
     2.7 -    "x - y \<equiv> x + - y" ..
     2.8 +    "x - (y\<Colon>complex) \<equiv> x + - y" ..
     2.9  
    2.10  lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
    2.11  by (simp add: complex_zero_def)
    2.12 @@ -116,7 +116,7 @@
    2.13      "inverse x \<equiv>
    2.14       Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
    2.15    complex_divide_def:
    2.16 -    "x / y \<equiv> x * inverse y" ..
    2.17 +    "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
    2.18  
    2.19  lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
    2.20  by (simp add: complex_one_def)
    2.21 @@ -195,7 +195,7 @@
    2.22  
    2.23  instance complex :: number
    2.24    complex_number_of_def:
    2.25 -    "number_of w \<equiv> of_int w" ..
    2.26 +    "number_of w \<equiv> of_int w \<Colon> complex" ..
    2.27  
    2.28  instance complex :: number_ring
    2.29  by (intro_classes, simp only: complex_number_of_def)
    2.30 @@ -213,10 +213,10 @@
    2.31  by (cases z rule: int_diff_cases) simp
    2.32  
    2.33  lemma complex_Re_number_of [simp]: "Re (number_of v) = number_of v"
    2.34 -unfolding number_ring_class.axioms by (rule complex_Re_of_int)
    2.35 +unfolding number_of_eq by (rule complex_Re_of_int)
    2.36  
    2.37  lemma complex_Im_number_of [simp]: "Im (number_of v) = 0"
    2.38 -unfolding number_ring_class.axioms by (rule complex_Im_of_int)
    2.39 +unfolding number_of_eq by (rule complex_Im_of_int)
    2.40  
    2.41  lemma Complex_eq_number_of [simp]:
    2.42    "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
     3.1 --- a/src/HOL/Finite_Set.thy	Thu Nov 29 07:55:46 2007 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Thu Nov 29 17:08:26 2007 +0100
     3.3 @@ -2689,7 +2689,7 @@
     3.4  lemmas [code func] = univ_bool
     3.5  
     3.6  instance * :: (finite, finite) finite
     3.7 -  "itself \<equiv> TYPE('a\<Colon>finite)"
     3.8 +  "itself \<equiv> TYPE('a \<times> 'b)"
     3.9  proof
    3.10    show "finite (UNIV :: ('a \<times> 'b) set)"
    3.11    proof (rule finite_Prod_UNIV)
    3.12 @@ -2703,7 +2703,7 @@
    3.13    unfolding UNIV_Times_UNIV ..
    3.14  
    3.15  instance "+" :: (finite, finite) finite
    3.16 -  "itself \<equiv> TYPE('a\<Colon>finite + 'b\<Colon>finite)"
    3.17 +  "itself \<equiv> TYPE('a + 'b)"
    3.18  proof
    3.19    have a: "finite (UNIV :: 'a set)" by (rule finite)
    3.20    have b: "finite (UNIV :: 'b set)" by (rule finite)
    3.21 @@ -2717,7 +2717,7 @@
    3.22    unfolding UNIV_Plus_UNIV ..
    3.23  
    3.24  instance set :: (finite) finite
    3.25 -  "itself \<equiv> TYPE('a\<Colon>finite set)"
    3.26 +  "itself \<equiv> TYPE('a set)"
    3.27  proof
    3.28    have "finite (UNIV :: 'a set)" by (rule finite)
    3.29    hence "finite (Pow (UNIV :: 'a set))"
    3.30 @@ -2732,7 +2732,7 @@
    3.31    by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
    3.32  
    3.33  instance "fun" :: (finite, finite) finite
    3.34 -  "itself \<equiv> TYPE('a\<Colon>finite \<Rightarrow> 'b\<Colon>finite)"
    3.35 +  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
    3.36  proof
    3.37    show "finite (UNIV :: ('a => 'b) set)"
    3.38    proof (rule finite_imageD)
     4.1 --- a/src/HOL/IntDef.thy	Thu Nov 29 07:55:46 2007 +0100
     4.2 +++ b/src/HOL/IntDef.thy	Thu Nov 29 17:08:26 2007 +0100
     4.3 @@ -36,7 +36,7 @@
     4.4  instance int :: minus
     4.5    minus_int_def:
     4.6      "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
     4.7 -  diff_int_def:  "z - w \<equiv> z + (-w)" ..
     4.8 +  diff_int_def:  "z - w \<equiv> z + (-w \<Colon> int)" ..
     4.9  
    4.10  instance int :: times
    4.11    mult_int_def: "z * w \<equiv>  Abs_Integ
    4.12 @@ -46,7 +46,7 @@
    4.13  instance int :: ord
    4.14    le_int_def:
    4.15     "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
    4.16 -  less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
    4.17 +  less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
    4.18  
    4.19  lemmas [code func del] = Zero_int_def One_int_def add_int_def
    4.20    minus_int_def mult_int_def le_int_def less_int_def
    4.21 @@ -218,8 +218,8 @@
    4.22    zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
    4.23  
    4.24  instance int :: distrib_lattice
    4.25 -  "inf \<equiv> min"
    4.26 -  "sup \<equiv> max"
    4.27 +  "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
    4.28 +  "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
    4.29    by intro_classes
    4.30      (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
    4.31  
     5.1 --- a/src/HOL/Library/Char_ord.thy	Thu Nov 29 07:55:46 2007 +0100
     5.2 +++ b/src/HOL/Library/Char_ord.thy	Thu Nov 29 17:08:26 2007 +0100
     5.3 @@ -39,8 +39,8 @@
     5.4  qed
     5.5  
     5.6  instance nibble :: distrib_lattice
     5.7 -    "inf \<equiv> min"
     5.8 -    "sup \<equiv> max"
     5.9 +  "(inf \<Colon> nibble \<Rightarrow> _) = min"
    5.10 +  "(sup \<Colon> nibble \<Rightarrow> _) = max"
    5.11    by default (auto simp add:
    5.12      inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    5.13  
    5.14 @@ -54,8 +54,8 @@
    5.15  lemmas [code func del] = char_less_eq_def char_less_def
    5.16  
    5.17  instance char :: distrib_lattice
    5.18 -    "inf \<equiv> min"
    5.19 -    "sup \<equiv> max"
    5.20 +  "(inf \<Colon> char \<Rightarrow> _) = min"
    5.21 +  "(sup \<Colon> char \<Rightarrow> _) = max"
    5.22    by default (auto simp add:
    5.23      inf_char_def sup_char_def min_max.sup_inf_distrib1)
    5.24  
     6.1 --- a/src/HOL/Library/Code_Index.thy	Thu Nov 29 07:55:46 2007 +0100
     6.2 +++ b/src/HOL/Library/Code_Index.thy	Thu Nov 29 17:08:26 2007 +0100
     6.3 @@ -143,7 +143,7 @@
     6.4    by simp
     6.5  
     6.6  instance index :: abs
     6.7 -  "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
     6.8 +  "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" ..
     6.9  
    6.10  lemma index_of_int [code func]:
    6.11    "index_of_int k = (if k = 0 then 0
     7.1 --- a/src/HOL/Library/Eval.thy	Thu Nov 29 07:55:46 2007 +0100
     7.2 +++ b/src/HOL/Library/Eval.thy	Thu Nov 29 17:08:26 2007 +0100
     7.3 @@ -35,16 +35,16 @@
     7.4  *}
     7.5  
     7.6  instance "prop" :: typ_of
     7.7 -  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
     7.8 +  "typ_of (T\<Colon>prop itself) \<equiv> STR ''prop'' {\<struct>} []" ..
     7.9  
    7.10  instance itself :: (typ_of) typ_of
    7.11 -  "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    7.12 +  "typ_of (T\<Colon>'a itself itself) \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    7.13  
    7.14  instance set :: (typ_of) typ_of
    7.15 -  "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    7.16 +  "typ_of (T\<Colon>'a set itself) \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    7.17  
    7.18  instance int :: typ_of
    7.19 -  "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
    7.20 +  "typ_of (T\<Colon>int itself) \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
    7.21  
    7.22  setup {*
    7.23  let
     8.1 --- a/src/HOL/Library/List_lexord.thy	Thu Nov 29 07:55:46 2007 +0100
     8.2 +++ b/src/HOL/Library/List_lexord.thy	Thu Nov 29 17:08:26 2007 +0100
     8.3 @@ -10,13 +10,11 @@
     8.4  begin
     8.5  
     8.6  instance list :: (ord) ord
     8.7 -  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
     8.8 -  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
     8.9 -
    8.10 -lemmas list_ord_defs [code func del] = list_less_def list_le_def
    8.11 +  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    8.12 +  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
    8.13  
    8.14  instance list :: (order) order
    8.15 -  apply (intro_classes, unfold list_ord_defs)
    8.16 +  apply (intro_classes, unfold list_less_def list_le_def)
    8.17    apply safe
    8.18    apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    8.19    apply simp
    8.20 @@ -35,13 +33,11 @@
    8.21    done
    8.22  
    8.23  instance list :: (linorder) distrib_lattice
    8.24 -  "inf \<equiv> min"
    8.25 -  "sup \<equiv> max"
    8.26 +  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    8.27 +  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    8.28    by intro_classes
    8.29      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    8.30  
    8.31 -lemmas [code func del] = inf_list_def sup_list_def
    8.32 -
    8.33  lemma not_less_Nil [simp]: "\<not> (x < [])"
    8.34    by (unfold list_less_def) simp
    8.35  
    8.36 @@ -52,13 +48,13 @@
    8.37    by (unfold list_less_def) simp
    8.38  
    8.39  lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
    8.40 -  by (unfold list_ord_defs, cases x) auto
    8.41 +  by (unfold list_le_def, cases x) auto
    8.42  
    8.43  lemma Nil_le_Cons [simp]: "[] \<le> x"
    8.44 -  by (unfold list_ord_defs, cases x) auto
    8.45 +  by (unfold list_le_def, cases x) auto
    8.46  
    8.47  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    8.48 -  by (unfold list_ord_defs) auto
    8.49 +  by (unfold list_le_def) auto
    8.50  
    8.51  lemma less_code [code func]:
    8.52    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
     9.1 --- a/src/HOL/Library/Parity.thy	Thu Nov 29 07:55:46 2007 +0100
     9.2 +++ b/src/HOL/Library/Parity.thy	Thu Nov 29 17:08:26 2007 +0100
     9.3 @@ -17,7 +17,7 @@
     9.4    "odd x \<equiv> \<not> even x"
     9.5  
     9.6  instance int :: even_odd
     9.7 -  even_def[presburger]: "even x \<equiv> x mod 2 = 0" ..
     9.8 +  even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
     9.9  
    9.10  instance nat :: even_odd
    9.11    even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
    10.1 --- a/src/HOL/Library/Product_ord.thy	Thu Nov 29 07:55:46 2007 +0100
    10.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Nov 29 17:08:26 2007 +0100
    10.3 @@ -10,30 +10,28 @@
    10.4  begin
    10.5  
    10.6  instance "*" :: (ord, ord) ord
    10.7 -  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
    10.8 -  prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
    10.9 -
   10.10 -lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def
   10.11 +  prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
   10.12 +  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
   10.13  
   10.14  lemma [code func]:
   10.15    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   10.16    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   10.17 -  unfolding prod_ord_defs by simp_all
   10.18 +  unfolding prod_le_def prod_less_def by simp_all
   10.19  
   10.20  lemma [code]:
   10.21    "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   10.22    "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   10.23 -  unfolding prod_ord_defs by simp_all
   10.24 +  unfolding prod_le_def prod_less_def by simp_all
   10.25  
   10.26  instance * :: (order, order) order
   10.27 -  by default (auto simp: prod_ord_defs intro: order_less_trans)
   10.28 +  by default (auto simp: prod_le_def prod_less_def intro: order_less_trans)
   10.29  
   10.30  instance * :: (linorder, linorder) linorder
   10.31    by default (auto simp: prod_le_def)
   10.32  
   10.33  instance * :: (linorder, linorder) distrib_lattice
   10.34 -  inf_prod_def: "inf \<equiv> min"
   10.35 -  sup_prod_def: "sup \<equiv> max"
   10.36 +  inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
   10.37 +  sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
   10.38    by intro_classes
   10.39      (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
   10.40  
    11.1 --- a/src/HOL/List.thy	Thu Nov 29 07:55:46 2007 +0100
    11.2 +++ b/src/HOL/List.thy	Thu Nov 29 17:08:26 2007 +0100
    11.3 @@ -2691,7 +2691,7 @@
    11.4  text{* The integers are an instance of the above class: *}
    11.5  
    11.6  instance int:: finite_intvl_succ
    11.7 -  successor_int_def: "successor == (%i. i+1)"
    11.8 +  successor_int_def: "successor == (%i\<Colon>int. i+1)"
    11.9  by intro_classes (simp_all add: successor_int_def)
   11.10  
   11.11  text{* Now @{term"[i..j::int]"} is defined for integers. *}
    12.1 --- a/src/HOL/Matrix/Matrix.thy	Thu Nov 29 07:55:46 2007 +0100
    12.2 +++ b/src/HOL/Matrix/Matrix.thy	Thu Nov 29 17:08:26 2007 +0100
    12.3 @@ -23,7 +23,7 @@
    12.4    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
    12.5  
    12.6  instance matrix :: (lordered_ab_group_add) abs
    12.7 -  abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
    12.8 +  abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
    12.9  
   12.10  instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
   12.11  proof 
    13.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Nov 29 07:55:46 2007 +0100
    13.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Nov 29 17:08:26 2007 +0100
    13.3 @@ -1281,7 +1281,7 @@
    13.4  
    13.5  instance matrix :: ("{ord, zero}") ord
    13.6    le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
    13.7 -  less_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
    13.8 +  less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
    13.9  
   13.10  instance matrix :: ("{order, zero}") order
   13.11  apply intro_classes
    14.1 --- a/src/HOL/Nat.thy	Thu Nov 29 07:55:46 2007 +0100
    14.2 +++ b/src/HOL/Nat.thy	Thu Nov 29 17:08:26 2007 +0100
    14.3 @@ -1488,8 +1488,8 @@
    14.4  text {* the lattice order on @{typ nat} *}
    14.5  
    14.6  instance nat :: distrib_lattice
    14.7 -  "inf \<equiv> min"
    14.8 -  "sup \<equiv> max"
    14.9 +  "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
   14.10 +  "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
   14.11    by intro_classes
   14.12      (simp_all add: inf_nat_def sup_nat_def)
   14.13  
    15.1 --- a/src/HOL/Numeral.thy	Thu Nov 29 07:55:46 2007 +0100
    15.2 +++ b/src/HOL/Numeral.thy	Thu Nov 29 17:08:26 2007 +0100
    15.3 @@ -203,16 +203,15 @@
    15.4    unfolding numeral_simps int_distrib by simp 
    15.5  
    15.6  
    15.7 -
    15.8  subsection {* Converting Numerals to Rings: @{term number_of} *}
    15.9  
   15.10 -axclass number_ring \<subseteq> number, comm_ring_1
   15.11 -  number_of_eq: "number_of k = of_int k"
   15.12 +class number_ring = number + comm_ring_1 +
   15.13 +  assumes number_of_eq: "number_of k = of_int k"
   15.14  
   15.15  text {* self-embedding of the integers *}
   15.16  
   15.17  instance int :: number_ring
   15.18 -  int_number_of_def: "number_of w \<equiv> of_int w"
   15.19 +  int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
   15.20    by intro_classes (simp only: int_number_of_def)
   15.21  
   15.22  lemmas [code func del] = int_number_of_def
    16.1 --- a/src/HOL/Orderings.thy	Thu Nov 29 07:55:46 2007 +0100
    16.2 +++ b/src/HOL/Orderings.thy	Thu Nov 29 17:08:26 2007 +0100
    16.3 @@ -930,7 +930,7 @@
    16.4  
    16.5  instance bool :: order 
    16.6    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
    16.7 -  less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    16.8 +  less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    16.9    by intro_classes (auto simp add: le_bool_def less_bool_def)
   16.10  lemmas [code func del] = le_bool_def less_bool_def
   16.11  
   16.12 @@ -968,7 +968,7 @@
   16.13  
   16.14  instance "fun" :: (type, ord) ord
   16.15    le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
   16.16 -  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
   16.17 +  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
   16.18  
   16.19  lemmas [code func del] = le_fun_def less_fun_def
   16.20  
    17.1 --- a/src/HOL/Real/PReal.thy	Thu Nov 29 07:55:46 2007 +0100
    17.2 +++ b/src/HOL/Real/PReal.thy	Thu Nov 29 17:08:26 2007 +0100
    17.3 @@ -212,8 +212,8 @@
    17.4    by intro_classes (rule preal_le_linear)
    17.5  
    17.6  instance preal :: distrib_lattice
    17.7 -  "inf \<equiv> min"
    17.8 -  "sup \<equiv> max"
    17.9 +  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
   17.10 +  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
   17.11    by intro_classes
   17.12      (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
   17.13  
    18.1 --- a/src/HOL/Real/Rational.thy	Thu Nov 29 07:55:46 2007 +0100
    18.2 +++ b/src/HOL/Real/Rational.thy	Thu Nov 29 17:08:26 2007 +0100
    18.3 @@ -362,8 +362,8 @@
    18.4  qed
    18.5  
    18.6  instance rat :: distrib_lattice
    18.7 -  "inf r s \<equiv> min r s"
    18.8 -  "sup r s \<equiv> max r s"
    18.9 +  "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
   18.10 +  "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
   18.11    by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
   18.12  
   18.13  instance rat :: ordered_field
    19.1 --- a/src/HOL/Real/RealDef.thy	Thu Nov 29 07:55:46 2007 +0100
    19.2 +++ b/src/HOL/Real/RealDef.thy	Thu Nov 29 17:08:26 2007 +0100
    19.3 @@ -66,7 +66,7 @@
    19.4    real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
    19.5  
    19.6  instance real :: sgn
    19.7 -  real_sgn_def: "sgn x == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
    19.8 +  real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
    19.9  
   19.10  subsection {* Equivalence relation over positive reals *}
   19.11  
   19.12 @@ -401,8 +401,8 @@
   19.13  done
   19.14  
   19.15  instance real :: distrib_lattice
   19.16 -  "inf x y \<equiv> min x y"
   19.17 -  "sup x y \<equiv> max x y"
   19.18 +  "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
   19.19 +  "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
   19.20    by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
   19.21  
   19.22  
    20.1 --- a/src/HOL/Set.thy	Thu Nov 29 07:55:46 2007 +0100
    20.2 +++ b/src/HOL/Set.thy	Thu Nov 29 17:08:26 2007 +0100
    20.3 @@ -145,7 +145,7 @@
    20.4  
    20.5  instance set :: (type) ord
    20.6    subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
    20.7 -  psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
    20.8 +  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
    20.9  lemmas [code func del] = subset_def psubset_def
   20.10  
   20.11  abbreviation
    21.1 --- a/src/HOL/SizeChange/Graphs.thy	Thu Nov 29 07:55:46 2007 +0100
    21.2 +++ b/src/HOL/SizeChange/Graphs.thy	Thu Nov 29 17:08:26 2007 +0100
    21.3 @@ -79,7 +79,7 @@
    21.4    graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
    21.5    graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
    21.6    "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
    21.7 -  "sup G H \<equiv> G + H"
    21.8 +  "sup (G \<Colon> ('a, 'b) graph)  H \<equiv> G + H"
    21.9    Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
   21.10    Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
   21.11  proof
   21.12 @@ -195,10 +195,10 @@
   21.13    "grpow 0 A = 1"
   21.14  | "grpow (Suc n) A = A * (grpow n A)"
   21.15  
   21.16 -instance graph :: (type, monoid_mult) 
   21.17 +instance graph :: (type, monoid_mult)
   21.18    "{semiring_1,idem_add,recpower,star}"
   21.19    graph_pow_def: "A ^ n == grpow n A"
   21.20 -  graph_star_def: "star G == (SUP n. G ^ n)" 
   21.21 +  graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)" 
   21.22  proof
   21.23    fix a b c :: "('a, 'b) graph"
   21.24    
    22.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 07:55:46 2007 +0100
    22.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 17:08:26 2007 +0100
    22.3 @@ -544,7 +544,7 @@
    22.4          |> not (null arities) ? (
    22.5              f arities css
    22.6              #-> (fn defs =>
    22.7 -              Class.prove_instance tac arities defs
    22.8 +              Instance.prove_instance tac arities defs
    22.9              #-> (fn defs =>
   22.10                after_qed arities css defs)))
   22.11        end;
    23.1 --- a/src/HOL/Tools/function_package/size.ML	Thu Nov 29 07:55:46 2007 +0100
    23.2 +++ b/src/HOL/Tools/function_package/size.ML	Thu Nov 29 17:08:26 2007 +0100
    23.3 @@ -38,7 +38,7 @@
    23.4      val n = Sign.arity_number thy tyco;
    23.5    in
    23.6      thy
    23.7 -    |> Class.prove_instance (Class.intro_classes_tac [])
    23.8 +    |> Instance.prove_instance (Class.intro_classes_tac [])
    23.9          [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
   23.10      |> snd
   23.11    end
    24.1 --- a/src/HOL/ex/Classpackage.thy	Thu Nov 29 07:55:46 2007 +0100
    24.2 +++ b/src/HOL/ex/Classpackage.thy	Thu Nov 29 17:08:26 2007 +0100
    24.3 @@ -13,14 +13,14 @@
    24.4    assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
    24.5  
    24.6  instance nat :: semigroup
    24.7 -  "m \<otimes> n \<equiv> m + n"
    24.8 +  "m \<otimes> n \<equiv> (m\<Colon>nat) + n"
    24.9  proof
   24.10    fix m n q :: nat 
   24.11    from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
   24.12  qed
   24.13  
   24.14  instance int :: semigroup
   24.15 -  "k \<otimes> l \<equiv> k + l"
   24.16 +  "k \<otimes> l \<equiv> (k\<Colon>int) + l"
   24.17  proof
   24.18    fix k l j :: int
   24.19    from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
   24.20 @@ -47,8 +47,8 @@
   24.21    assumes neutl: "\<one> \<otimes> x = x"
   24.22  
   24.23  instance nat :: monoidl and int :: monoidl
   24.24 -  "\<one> \<equiv> 0"
   24.25 -  "\<one> \<equiv> 0"
   24.26 +  "\<one> \<equiv> (0\<Colon>nat)"
   24.27 +  "\<one> \<equiv> (0\<Colon>int)"
   24.28  proof
   24.29    fix n :: nat
   24.30    from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
    25.1 --- a/src/Pure/Isar/class.ML	Thu Nov 29 07:55:46 2007 +0100
    25.2 +++ b/src/Pure/Isar/class.ML	Thu Nov 29 17:08:26 2007 +0100
    25.3 @@ -57,16 +57,7 @@
    25.4  
    25.5    (*old instance layer*)
    25.6    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    25.7 -  val instance: arity list -> ((bstring * Attrib.src list) * term) list
    25.8 -    -> (thm list -> theory -> theory)
    25.9 -    -> theory -> Proof.state
   25.10 -  val instance_cmd: (bstring * xstring list * xstring) list
   25.11 -    -> ((bstring * Attrib.src list) * xstring) list
   25.12 -    -> (thm list -> theory -> theory)
   25.13 -    -> theory -> Proof.state
   25.14 -  val prove_instance: tactic -> arity list
   25.15 -    -> ((bstring * Attrib.src list) * term) list
   25.16 -    -> theory -> thm list * theory
   25.17 +  val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state
   25.18  end;
   25.19  
   25.20  structure Class : CLASS =
   25.21 @@ -150,6 +141,8 @@
   25.22  
   25.23  val instance_arity =
   25.24    gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   25.25 +val instance_arity_cmd =
   25.26 +  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
   25.27  val classrel =
   25.28    gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
   25.29      AxClass.add_classrel I o single;
   25.30 @@ -221,7 +214,7 @@
   25.31      val SOME class = AxClass.class_of_param thy c;
   25.32      val SOME tyco = inst_tyco thy (c, ty);
   25.33      val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   25.34 -    val c' = NameSpace.base c;
   25.35 +    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
   25.36      val ty' = Type.strip_sorts ty;
   25.37    in
   25.38      thy
   25.39 @@ -253,137 +246,6 @@
   25.40    end;
   25.41  
   25.42  
   25.43 -(* legacy *)
   25.44 -
   25.45 -fun add_inst_def (class, tyco) (c, ty) thy =
   25.46 -  let
   25.47 -    val tyco_base = Sign.base_name tyco;
   25.48 -    val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst";
   25.49 -    val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base;
   25.50 -  in
   25.51 -    thy
   25.52 -    |> Sign.sticky_prefix name_inst
   25.53 -    |> Sign.declare_const [] (c_inst_base, ty, NoSyn)
   25.54 -    |-> (fn const as Const (c_inst, _) =>
   25.55 -      PureThy.add_defs_i false
   25.56 -        [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])]
   25.57 -      #-> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm)))
   25.58 -    |> Sign.restore_naming thy
   25.59 -  end;
   25.60 -
   25.61 -fun add_inst_def' (class, tyco) (c, ty) thy =
   25.62 -  if case Symtab.lookup (fst (InstData.get thy)) c
   25.63 -   of NONE => true
   25.64 -    | SOME tab => is_none (Symtab.lookup tab tyco)
   25.65 -  then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
   25.66 -  else thy;
   25.67 -
   25.68 -fun add_def ((class, tyco), ((name, prop), atts)) thy =
   25.69 -  let
   25.70 -    val ((lhs as Const (c, ty), args), rhs) =
   25.71 -      (apfst Term.strip_comb o Logic.dest_equals) prop;
   25.72 -  in
   25.73 -    thy
   25.74 -    |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
   25.75 -    |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
   25.76 -  end;
   25.77 -
   25.78 -
   25.79 -(** instances with implicit parameter handling **)
   25.80 -
   25.81 -local
   25.82 -
   25.83 -fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
   25.84 -  let
   25.85 -    val ctxt = ProofContext.init thy;
   25.86 -    val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
   25.87 -    val ((c, ty), _) = Sign.cert_def ctxt t;
   25.88 -    val atts = map (prep_att thy) raw_atts;
   25.89 -    val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
   25.90 -    val name = case raw_name
   25.91 -     of "" => NONE
   25.92 -      | _ => SOME raw_name;
   25.93 -  in (c, (insts, ((name, t), atts))) end;
   25.94 -
   25.95 -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
   25.96 -fun read_def thy = gen_read_def thy (K I) (K I);
   25.97 -
   25.98 -fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   25.99 -  let
  25.100 -    val arities = map (prep_arity theory) raw_arities;
  25.101 -    val _ = if null arities then error "At least one arity must be given" else ();
  25.102 -    val _ = case (duplicates (op =) o map #1) arities
  25.103 -     of [] => ()
  25.104 -      | dupl_tycos => error ("Type constructors occur more than once in arities: "
  25.105 -          ^ commas_quote dupl_tycos);
  25.106 -    fun get_consts_class tyco ty class =
  25.107 -      let
  25.108 -        val cs = (these o try (#params o AxClass.get_info theory)) class;
  25.109 -        val subst_ty = map_type_tfree (K ty);
  25.110 -      in
  25.111 -        map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
  25.112 -      end;
  25.113 -    fun get_consts_sort (tyco, asorts, sort) =
  25.114 -      let
  25.115 -        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
  25.116 -          (Name.names Name.context Name.aT asorts))
  25.117 -      in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
  25.118 -    val cs = maps get_consts_sort arities;
  25.119 -    fun mk_typnorm thy (ty, ty_sc) =
  25.120 -      case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
  25.121 -       of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
  25.122 -        | NONE => NONE;
  25.123 -    fun read_defs defs cs thy_read =
  25.124 -      let
  25.125 -        fun read raw_def cs =
  25.126 -          let
  25.127 -            val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
  25.128 -            val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
  25.129 -            val ((class, tyco), ty') = case AList.lookup (op =) cs c
  25.130 -             of NONE => error ("Illegal definition for constant " ^ quote c)
  25.131 -              | SOME class_ty => class_ty;
  25.132 -            val name = case name_opt
  25.133 -             of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
  25.134 -              | SOME name => name;
  25.135 -            val t' = case mk_typnorm thy_read (ty', ty)
  25.136 -             of NONE => error ("Illegal definition for constant " ^
  25.137 -                  quote (c ^ "::" ^ setmp show_sorts true
  25.138 -                    (Sign.string_of_typ thy_read) ty))
  25.139 -              | SOME norm => map_types norm t
  25.140 -          in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
  25.141 -      in fold_map read defs cs end;
  25.142 -    val (defs, other_cs) = read_defs raw_defs cs
  25.143 -      (fold Sign.primitive_arity arities (Theory.copy theory));
  25.144 -    fun after_qed' cs defs =
  25.145 -      fold Sign.add_const_constraint (map (apsnd SOME) cs)
  25.146 -      #> after_qed defs;
  25.147 -  in
  25.148 -    theory
  25.149 -    |> fold_map get_remove_global_constraint (map fst cs |> distinct (op =))
  25.150 -    ||>> fold_map add_def defs
  25.151 -    ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
  25.152 -    |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
  25.153 -  end;
  25.154 -
  25.155 -fun tactic_proof tac f arities defs =
  25.156 -  fold (fn arity => AxClass.prove_arity arity tac) arities
  25.157 -  #> f
  25.158 -  #> pair defs;
  25.159 -
  25.160 -in
  25.161 -
  25.162 -val instance = gen_instance Sign.cert_arity read_def
  25.163 -  (fn f => fn arities => fn defs => instance_arity f arities);
  25.164 -val instance_cmd = gen_instance Sign.read_arity read_def_cmd
  25.165 -  (fn f => fn arities => fn defs => instance_arity f arities);
  25.166 -fun prove_instance tac arities defs =
  25.167 -  gen_instance Sign.cert_arity read_def
  25.168 -    (tactic_proof tac) arities defs (K I);
  25.169 -
  25.170 -end; (*local*)
  25.171 -
  25.172 -
  25.173 -
  25.174  (** class data **)
  25.175  
  25.176  datatype class_data = ClassData of {
  25.177 @@ -1008,7 +870,7 @@
  25.178  
  25.179      fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
  25.180           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
  25.181 -             of SOME (_, ty') => Type.typ_match tsig (ty, ty')
  25.182 +             of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
  25.183                | NONE => I)
  25.184            | NONE => I)
  25.185        | check_improve _ = I;
  25.186 @@ -1057,6 +919,7 @@
  25.187       of [] => ()
  25.188        | dupl_tycos => error ("Type constructors occur more than once in arities: "
  25.189            ^ commas_quote dupl_tycos);
  25.190 +    val _ = map (map (the_class_data thy) o #3) arities;
  25.191      val ty_insts = map (fn (tyco, sorts, _) =>
  25.192          (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
  25.193        arities;
  25.194 @@ -1064,12 +927,11 @@
  25.195      fun type_name "*" = "prod"
  25.196        | type_name "+" = "sum"
  25.197        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
  25.198 -    fun get_param tyco sorts (param, (c, ty)) =
  25.199 -      ((unoverload_const thy (c, ty), tyco),
  25.200 -        (param ^ "_" ^ type_name tyco,
  25.201 -          map_atyps (K (ty_inst tyco)) ty));
  25.202 +    fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco)
  25.203 +      then NONE else SOME ((unoverload_const thy (c, ty), tyco),
  25.204 +        (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty));
  25.205      fun get_params (tyco, sorts, sort) =
  25.206 -      map (get_param tyco sorts) (these_params thy sort)
  25.207 +      map_filter (get_param tyco sorts) (these_params thy sort)
  25.208      val params = maps get_params arities;
  25.209    in
  25.210      thy
  25.211 @@ -1099,8 +961,8 @@
  25.212    Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
  25.213  
  25.214  fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
  25.215 -  fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
  25.216 -    (fn {context, ...} => tac context)) lthy) I;
  25.217 +  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
  25.218 +    (fn {context, ...} => tac context)) ts) lthy) I;
  25.219  
  25.220  fun conclude_instantiation lthy =
  25.221    let
  25.222 @@ -1121,7 +983,7 @@
  25.223        let
  25.224          val SOME class = AxClass.class_of_param thy c;
  25.225          val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
  25.226 -        val c' = NameSpace.base c;
  25.227 +        val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
  25.228          val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
  25.229          val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
  25.230        in
    26.1 --- a/src/Pure/Isar/instance.ML	Thu Nov 29 07:55:46 2007 +0100
    26.2 +++ b/src/Pure/Isar/instance.ML	Thu Nov 29 17:08:26 2007 +0100
    26.3 @@ -10,7 +10,6 @@
    26.4    val instantiate: arity list -> (local_theory -> local_theory)
    26.5      -> (Proof.context -> tactic) -> theory -> theory
    26.6    val instance: arity list -> ((bstring * Attrib.src list) * term) list
    26.7 -    -> (thm list -> theory -> theory)
    26.8      -> theory -> Proof.state
    26.9    val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
   26.10      -> theory -> thm list * theory
   26.11 @@ -18,7 +17,6 @@
   26.12    val instantiation_cmd: (xstring * sort * xstring) list
   26.13      -> theory -> local_theory
   26.14    val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
   26.15 -    -> (thm list -> theory -> theory)
   26.16      -> theory -> Proof.state
   26.17  end;
   26.18  
   26.19 @@ -35,8 +33,9 @@
   26.20    #> LocalTheory.exit
   26.21    #> ProofContext.theory_of;
   26.22  
   26.23 -fun gen_instance prep_arity prep_attr parse_term do_proof raw_arities defs after_qed thy =
   26.24 +fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
   26.25    let
   26.26 +    val arities = map (prep_arity thy) raw_arities;
   26.27      fun export_defs ctxt = 
   26.28        let
   26.29          val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
   26.30 @@ -54,8 +53,9 @@
   26.31        let
   26.32          val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
   26.33        in Specification.definition def' ctxt end;
   26.34 -    val arities = map (prep_arity thy) raw_arities;
   26.35 -  in
   26.36 +  in if not (null defs) orelse forall (fn (_, _, sort) =>
   26.37 +      forall (Class.is_class thy) sort) arities
   26.38 +  then
   26.39      thy
   26.40      |> TheoryTarget.instantiation arities
   26.41      |> `(fn ctxt => map (mk_def ctxt) defs)
   26.42 @@ -64,15 +64,21 @@
   26.43      ||> LocalTheory.exit
   26.44      ||> ProofContext.theory_of
   26.45      ||> TheoryTarget.instantiation arities
   26.46 -    |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs)))
   26.47 +    |-> (fn defs => do_proof defs)
   26.48 +  else
   26.49 +    thy
   26.50 +    |> do_proof' arities
   26.51    end;
   26.52  
   26.53  val instance = gen_instance Sign.cert_arity (K I) (K I)
   26.54 -  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
   26.55 +  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
   26.56  val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
   26.57 -  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
   26.58 +  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
   26.59  fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
   26.60 -  (fn defs => fn after_qed => Class.prove_instantiation_instance (K tac)
   26.61 -    #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
   26.62 +  (fn defs => Class.prove_instantiation_instance (K tac)
   26.63 +    #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs)
   26.64 +   (pair [] o ProofContext.theory_of o Proof.global_terminal_proof
   26.65 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   26.66 +      oo Class.instance_arity I) arities defs;
   26.67  
   26.68  end;
    27.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 29 07:55:46 2007 +0100
    27.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 29 17:08:26 2007 +0100
    27.3 @@ -453,10 +453,8 @@
    27.4  val _ =
    27.5    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    27.6    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    27.7 -    P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    27.8 -      >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
    27.9      P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
   27.10 -      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
   27.11 +      >> (fn (arities, defs) => Instance.instance_cmd arities defs))
   27.12      >> (Toplevel.print oo Toplevel.theory_to_proof)
   27.13    || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
   27.14