improved
authorhaftmann
Wed Dec 05 14:15:51 2007 +0100 (2007-12-05)
changeset 2553601753a944433
parent 25535 4975b7529a14
child 25537 55017c8b0a24
improved
src/HOL/Library/Eval.thy
src/HOL/ex/ExecutableContent.thy
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Wed Dec 05 14:15:48 2007 +0100
     1.2 +++ b/src/HOL/Library/Eval.thy	Wed Dec 05 14:15:51 2007 +0100
     1.3 @@ -18,47 +18,64 @@
     1.4  structure TypOf =
     1.5  struct
     1.6  
     1.7 -val class_typ_of = Sign.intern_class @{theory} "typ_of";
     1.8 -
     1.9 -fun term_typ_of_type ty =
    1.10 +fun mk ty =
    1.11    Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    1.12      $ Logic.mk_type ty;
    1.13  
    1.14 -fun mk_typ_of_def ty =
    1.15 -  let
    1.16 -    val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    1.17 -      $ Free ("x", Term.itselfT ty)
    1.18 -    val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty
    1.19 -  in Logic.mk_equals (lhs, rhs) end;
    1.20 -
    1.21 -end;
    1.22 +end
    1.23  *}
    1.24  
    1.25 -instance "prop" :: typ_of
    1.26 -  "typ_of (T\<Colon>prop itself) \<equiv> STR ''prop'' {\<struct>} []" ..
    1.27 -
    1.28 -instance itself :: (typ_of) typ_of
    1.29 -  "typ_of (T\<Colon>'a itself itself) \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    1.30 -
    1.31 -instance set :: (typ_of) typ_of
    1.32 -  "typ_of (T\<Colon>'a set itself) \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    1.33 -
    1.34 -instance int :: typ_of
    1.35 -  "typ_of (T\<Colon>int itself) \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
    1.36 -
    1.37  setup {*
    1.38  let
    1.39 -  fun mk arities _ thy =
    1.40 -    (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def
    1.41 -      (Type (tyco,
    1.42 -        map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
    1.43 -  fun hook specs =
    1.44 -    DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    1.45 -      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    1.46 -      [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
    1.47 -in DatatypeCodegen.add_codetypes_hook hook end
    1.48 +  fun define_typ_of ty lthy =
    1.49 +    let
    1.50 +      val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    1.51 +        $ Free ("T", Term.itselfT ty);
    1.52 +      val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
    1.53 +      val eq = Class.prep_spec lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    1.54 +    in lthy |> Specification.definition (NONE, (("", []), eq)) end;
    1.55 +  fun interpretator tyco thy =
    1.56 +    let
    1.57 +      val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
    1.58 +      val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
    1.59 +    in
    1.60 +      thy
    1.61 +      |> Instance.instantiate ([tyco], sorts, @{sort typ_of})
    1.62 +           (define_typ_of ty) ((K o K) (Class.intro_classes_tac []))
    1.63 +    end;
    1.64 +in TypedefPackage.interpretation interpretator end
    1.65  *}
    1.66  
    1.67 +instantiation "prop" :: typ_of
    1.68 +begin
    1.69 +
    1.70 +definition
    1.71 +  "typ_of (T\<Colon>prop itself) = STR ''prop'' {\<struct>} []"
    1.72 +
    1.73 +instance ..
    1.74 +
    1.75 +end
    1.76 +
    1.77 +instantiation itself :: (typ_of) typ_of
    1.78 +begin
    1.79 +
    1.80 +definition
    1.81 +  "typ_of (T\<Colon>'a itself itself) = STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
    1.82 +
    1.83 +instance ..
    1.84 +
    1.85 +end
    1.86 +
    1.87 +instantiation set :: (typ_of) typ_of
    1.88 +begin
    1.89 + 
    1.90 +definition
    1.91 +  "typ_of (T\<Colon>'a set itself) = STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
    1.92 +
    1.93 +instance ..
    1.94 +
    1.95 +end
    1.96 +
    1.97  
    1.98  subsection {* @{text term_of} class *}
    1.99  
   1.100 @@ -83,7 +100,7 @@
   1.101            val lhs : term = term_term_of dty $ c;
   1.102            val rhs : term = Pure_term.mk_term
   1.103              (fn (v, ty) => term_term_of ty $ Free (v, ty))
   1.104 -            (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
   1.105 +            (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
   1.106          in
   1.107            HOLogic.mk_eq (lhs, rhs)
   1.108          end;
   1.109 @@ -101,24 +118,43 @@
   1.110      PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   1.111    fun thy_def ((name, atts), t) =
   1.112      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   1.113 -  fun mk arities css _ thy =
   1.114 +  fun prep_dtyp thy vs tyco =
   1.115 +    let
   1.116 +      val (_, cs) = DatatypePackage.the_datatype_spec thy tyco;
   1.117 +      val prep_typ = map_atyps (fn TFree (v, sort) =>
   1.118 +        TFree (v, (the o AList.lookup (op =) vs) v));
   1.119 +      fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)),
   1.120 +        map Free (Name.names Name.context "a" tys));
   1.121 +    in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end;
   1.122 +  fun prep thy tycos =
   1.123      let
   1.124 -      val (_, asorts, _) :: _ = arities;
   1.125 -      val vs = Name.names Name.context "'a" asorts;
   1.126 +      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
   1.127 +      val tyco = hd tycos;
   1.128 +      val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco;
   1.129 +      val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos;
   1.130 +      fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #>
   1.131 +            fold add_tycos tys
   1.132 +        | add_tycos _ = I;
   1.133 +      val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos;
   1.134 +      val sorts = map (inter_sort o snd) vs_proto;
   1.135 +      val vs = map fst vs_proto ~~ sorts;
   1.136 +      val css = map (prep_dtyp thy vs) tycos;
   1.137        val defs = map (TermOf.mk_terms_of_defs vs) css;
   1.138        val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
   1.139 -    in
   1.140 -      thy
   1.141 -      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
   1.142 -      |> snd
   1.143 +    in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
   1.144 +        andalso not (tycos = [@{type_name typ}])
   1.145 +      then SOME (sorts, defs')
   1.146 +      else NONE
   1.147      end;
   1.148 -  fun hook specs =
   1.149 -    if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
   1.150 -    else
   1.151 -      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
   1.152 -      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   1.153 -      [TermOf.class_term_of] ((K o K o pair) []) mk
   1.154 -in DatatypeCodegen.add_codetypes_hook hook end
   1.155 +  fun interpretator tycos thy = case prep thy tycos
   1.156 +   of SOME (sorts, defs) =>
   1.157 +      thy
   1.158 +      |> Instance.instantiate (tycos, sorts, @{sort term_of})
   1.159 +           (pair ()) ((K o K) (Class.intro_classes_tac []))
   1.160 +      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs
   1.161 +      |> snd
   1.162 +    | NONE => thy;
   1.163 +  in DatatypePackage.interpretation interpretator end
   1.164  *}
   1.165  
   1.166  abbreviation
     2.1 --- a/src/HOL/ex/ExecutableContent.thy	Wed Dec 05 14:15:48 2007 +0100
     2.2 +++ b/src/HOL/ex/ExecutableContent.thy	Wed Dec 05 14:15:51 2007 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  theory ExecutableContent
     2.5  imports
     2.6    Main
     2.7 -  (*Eval*)
     2.8 +  Eval
     2.9    "~~/src/HOL/ex/Records"
    2.10    AssocList
    2.11    Binomial
     3.1 --- a/src/Pure/Isar/class.ML	Wed Dec 05 14:15:48 2007 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Wed Dec 05 14:15:51 2007 +0100
     3.3 @@ -31,7 +31,8 @@
     3.4    val print_classes: theory -> unit
     3.5  
     3.6    (*instances*)
     3.7 -  val init_instantiation: arity list -> theory -> local_theory
     3.8 +  val init_instantiation: string list * sort list * sort -> theory -> local_theory
     3.9 +  val prep_spec: local_theory -> term -> term
    3.10    val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    3.11    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    3.12    val conclude_instantiation: local_theory -> local_theory
    3.13 @@ -56,8 +57,8 @@
    3.14    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    3.15  
    3.16    (*old instance layer*)
    3.17 -  val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    3.18 -  val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state
    3.19 +  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    3.20 +  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    3.21  end;
    3.22  
    3.23  structure Class : CLASS =
    3.24 @@ -134,7 +135,7 @@
    3.25      thy
    3.26      |> ProofContext.init
    3.27      |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
    3.28 -        o maps (mk_prop thy)) insts)
    3.29 +        o mk_prop thy) insts)
    3.30    end;
    3.31  
    3.32  in
    3.33 @@ -144,11 +145,9 @@
    3.34  val instance_arity_cmd =
    3.35    gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
    3.36  val classrel =
    3.37 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
    3.38 -    AxClass.add_classrel I o single;
    3.39 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
    3.40  val classrel_cmd =
    3.41 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
    3.42 -    AxClass.add_classrel I o single;
    3.43 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
    3.44  
    3.45  end; (*local*)
    3.46  
    3.47 @@ -826,14 +825,14 @@
    3.48  (* bookkeeping *)
    3.49  
    3.50  datatype instantiation = Instantiation of {
    3.51 -  arities: arity list,
    3.52 +  arities: string list * sort list * sort,
    3.53    params: ((string * string) * (string * typ)) list
    3.54  }
    3.55  
    3.56  structure Instantiation = ProofDataFun
    3.57  (
    3.58    type T = instantiation
    3.59 -  fun init _ = Instantiation { arities = [], params = [] };
    3.60 +  fun init _ = Instantiation { arities = ([], [], []), params = [] };
    3.61  );
    3.62  
    3.63  fun mk_instantiation (arities, params) =
    3.64 @@ -844,7 +843,7 @@
    3.65    (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
    3.66  
    3.67  fun the_instantiation lthy = case get_instantiation lthy
    3.68 - of { arities = [], ... } => error "No instantiation target"
    3.69 + of { arities = ([], [], []), ... } => error "No instantiation target"
    3.70    | data => data;
    3.71  
    3.72  val instantiation_params = #params o get_instantiation;
    3.73 @@ -859,6 +858,19 @@
    3.74  
    3.75  (* syntax *)
    3.76  
    3.77 +fun subst_param thy params = map_aterms (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
    3.78 +     of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    3.79 +         of SOME v_ty => Free v_ty
    3.80 +          | NONE => t)
    3.81 +      | NONE => t)
    3.82 +  | t => t);
    3.83 +
    3.84 +fun prep_spec lthy =
    3.85 +  let
    3.86 +    val thy = ProofContext.theory_of lthy;
    3.87 +    val params = instantiation_params lthy;
    3.88 +  in subst_param thy params end;
    3.89 +
    3.90  fun inst_term_check ts lthy =
    3.91    let
    3.92      val params = instantiation_params lthy;
    3.93 @@ -873,12 +885,7 @@
    3.94        | check_improve _ = I;
    3.95      val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
    3.96      val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
    3.97 -    val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
    3.98 -         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    3.99 -             of SOME v_ty => Free v_ty
   3.100 -              | NONE => t)
   3.101 -          | NONE => t)
   3.102 -      | t => t) ts';
   3.103 +    val ts'' = map (subst_param thy params) ts';
   3.104    in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
   3.105  
   3.106  fun inst_term_uncheck ts lthy =
   3.107 @@ -908,33 +915,24 @@
   3.108      explode #> scan_valids #> implode
   3.109    end;
   3.110  
   3.111 -fun init_instantiation arities thy =
   3.112 +fun init_instantiation (tycos, sorts, sort) thy =
   3.113    let
   3.114 -    val _ = if null arities then error "At least one arity must be given" else ();
   3.115 -    val _ = case (duplicates (op =) o map #1) arities
   3.116 -     of [] => ()
   3.117 -      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   3.118 -          ^ commas_quote dupl_tycos);
   3.119 -    val _ = map (map (the_class_data thy) o #3) arities;
   3.120 -    val ty_insts = map (fn (tyco, sorts, _) =>
   3.121 -        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   3.122 -      arities;
   3.123 -    val ty_inst = the o AList.lookup (op =) ty_insts;
   3.124 +    val _ = if null tycos then error "At least one arity must be given" else ();
   3.125 +    val _ = map (the_class_data thy) sort;
   3.126 +    val vs = map TFree (Name.names Name.context Name.aT sorts);
   3.127      fun type_name "*" = "prod"
   3.128        | type_name "+" = "sum"
   3.129        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   3.130 -    fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco)
   3.131 +    fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco)
   3.132        then NONE else SOME ((unoverload_const thy (c, ty), tyco),
   3.133 -        (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty));
   3.134 -    fun get_params (tyco, sorts, sort) =
   3.135 -      map_filter (get_param tyco sorts) (these_params thy sort)
   3.136 -    val params = maps get_params arities;
   3.137 +        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
   3.138 +    val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
   3.139    in
   3.140      thy
   3.141      |> ProofContext.init
   3.142 -    |> Instantiation.put (mk_instantiation (arities, params))
   3.143 -    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   3.144 -    |> fold ProofContext.add_arity arities
   3.145 +    |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
   3.146 +    |> fold (Variable.declare_term o Logic.mk_type) vs
   3.147 +    |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
   3.148      |> Context.proof_map (
   3.149          Syntax.add_term_check 0 "instance" inst_term_check
   3.150          #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
   3.151 @@ -942,8 +940,8 @@
   3.152  
   3.153  fun gen_instantiation_instance do_proof after_qed lthy =
   3.154    let
   3.155 -    val arities = (#arities o the_instantiation) lthy;
   3.156 -    val arities_proof = maps Logic.mk_arities arities;
   3.157 +    val (tycos, sorts, sort) = (#arities o the_instantiation) lthy;
   3.158 +    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   3.159      fun after_qed' results =
   3.160        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   3.161        #> after_qed;
   3.162 @@ -962,6 +960,7 @@
   3.163  fun conclude_instantiation lthy =
   3.164    let
   3.165      val { arities, params } = the_instantiation lthy;
   3.166 +    val (tycos, sorts, sort) = arities;
   3.167      val thy = ProofContext.theory_of lthy;
   3.168      (*val _ = map (fn (tyco, sorts, sort) =>
   3.169        if Sign.of_sort thy
   3.170 @@ -970,8 +969,8 @@
   3.171          arities; FIXME activate when old instance command is gone*)
   3.172      val params_of = maps (these o try (#params o AxClass.get_info thy))
   3.173        o Sign.complete_sort thy;
   3.174 -    val missing_params = arities
   3.175 -      |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
   3.176 +    val missing_params = tycos
   3.177 +      |> maps (fn tyco => params_of sort |> map (rpair tyco))
   3.178        |> filter_out (can (inst thy) o apfst fst);
   3.179      fun declare_missing ((c, ty0), tyco) thy =
   3.180      (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
     4.1 --- a/src/Pure/Isar/instance.ML	Wed Dec 05 14:15:48 2007 +0100
     4.2 +++ b/src/Pure/Isar/instance.ML	Wed Dec 05 14:15:51 2007 +0100
     4.3 @@ -7,35 +7,38 @@
     4.4  
     4.5  signature INSTANCE =
     4.6  sig
     4.7 -  val instantiate: arity list -> (local_theory -> local_theory)
     4.8 -    -> (Proof.context -> tactic) -> theory -> theory
     4.9 -  val instance: arity list -> ((bstring * Attrib.src list) * term) list
    4.10 -    -> theory -> Proof.state
    4.11 -  val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
    4.12 -    -> theory -> thm list * theory
    4.13 +  val instantiate: string list * sort list * sort -> (local_theory -> 'a * local_theory)
    4.14 +    -> (Proof.context -> 'a -> tactic) -> theory -> theory
    4.15  
    4.16 -  val instantiation_cmd: (xstring * sort * xstring) list
    4.17 -    -> theory -> local_theory
    4.18 -  val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
    4.19 +  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
    4.20 +  val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list
    4.21      -> theory -> Proof.state
    4.22  end;
    4.23  
    4.24  structure Instance : INSTANCE =
    4.25  struct
    4.26  
    4.27 +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    4.28 +  let
    4.29 +    val all_arities = map (fn raw_tyco => Sign.read_arity thy
    4.30 +      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    4.31 +    val tycos = map #1 all_arities;
    4.32 +    val (_, sorts, sort) = hd all_arities;
    4.33 +  in (tycos, sorts, sort) end;
    4.34 +
    4.35  fun instantiation_cmd raw_arities thy =
    4.36 -  TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy;
    4.37 +  TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
    4.38  
    4.39  fun instantiate arities f tac =
    4.40    TheoryTarget.instantiation arities
    4.41    #> f
    4.42 -  #> Class.prove_instantiation_instance tac
    4.43 +  #-> (fn result => Class.prove_instantiation_instance (fn ctxt => tac ctxt result))
    4.44    #> LocalTheory.exit
    4.45    #> ProofContext.theory_of;
    4.46  
    4.47  fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
    4.48    let
    4.49 -    val arities = map (prep_arity thy) raw_arities;
    4.50 +    val (tyco, sorts, sort) = prep_arity thy raw_arities;
    4.51      fun export_defs ctxt = 
    4.52        let
    4.53          val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
    4.54 @@ -53,32 +56,21 @@
    4.55        let
    4.56          val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
    4.57        in Specification.definition def' ctxt end;
    4.58 -  in if not (null defs) orelse forall (fn (_, _, sort) =>
    4.59 -      forall (Class.is_class thy) sort) arities
    4.60 +  in if not (null defs) orelse forall (Class.is_class thy) sort
    4.61    then
    4.62      thy
    4.63 -    |> TheoryTarget.instantiation arities
    4.64 +    |> TheoryTarget.instantiation ([tyco], sorts, sort)
    4.65      |> `(fn ctxt => map (mk_def ctxt) defs)
    4.66      |-> (fn defs => fold_map Specification.definition defs)
    4.67      |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
    4.68      ||> LocalTheory.reinit
    4.69 -    (*||> ProofContext.theory_of
    4.70 -    ||> TheoryTarget.instantiation arities*)
    4.71      |-> (fn defs => do_proof defs)
    4.72    else
    4.73      thy
    4.74 -    |> do_proof' arities
    4.75 +    |> do_proof' (tyco, sorts, sort)
    4.76    end;
    4.77  
    4.78 -val instance = gen_instance Sign.cert_arity (K I) (K I)
    4.79 -  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
    4.80  val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
    4.81    (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
    4.82 -fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
    4.83 -  (fn defs => Class.prove_instantiation_instance (K tac)
    4.84 -    #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs)
    4.85 -   (pair [] o ProofContext.theory_of o Proof.global_terminal_proof
    4.86 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    4.87 -      oo Class.instance_arity I) arities defs;
    4.88  
    4.89  end;
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Dec 05 14:15:48 2007 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 05 14:15:51 2007 +0100
     5.3 @@ -446,15 +446,15 @@
     5.4  
     5.5  val _ =
     5.6    OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
     5.7 -   (P.and_list1 P.arity --| P.begin
     5.8 +   (P.multi_arity --| P.begin
     5.9       >> (fn arities => Toplevel.print o
    5.10           Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    5.11  
    5.12  val _ =
    5.13    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    5.14    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    5.15 -    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    5.16 -      >> (fn (arities, defs) => Instance.instance_cmd arities defs))
    5.17 +    P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    5.18 +      >> (fn (arity, defs) => Instance.instance_cmd arity defs))
    5.19      >> (Toplevel.print oo Toplevel.theory_to_proof)
    5.20    || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
    5.21  
     6.1 --- a/src/Pure/Isar/overloading.ML	Wed Dec 05 14:15:48 2007 +0100
     6.2 +++ b/src/Pure/Isar/overloading.ML	Wed Dec 05 14:15:51 2007 +0100
     6.3 @@ -8,6 +8,7 @@
     6.4  signature OVERLOADING =
     6.5  sig
     6.6    val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
     6.7 +  val prep_spec: local_theory -> term -> term
     6.8    val conclude: local_theory -> local_theory
     6.9    val declare: string * typ -> theory -> term * theory
    6.10    val confirm: string -> local_theory -> local_theory
    6.11 @@ -45,14 +46,21 @@
    6.12  
    6.13  (* syntax *)
    6.14  
    6.15 +fun subst_operation overloading = map_aterms (fn t as Const (c, ty) =>
    6.16 +    (case AList.lookup (op =) overloading (c, ty)
    6.17 +     of SOME (v, _) => Free (v, ty)
    6.18 +      | NONE => t)
    6.19 +  | t => t);
    6.20 +
    6.21 +fun prep_spec lthy =
    6.22 +  let
    6.23 +    val overloading = get_overloading lthy;
    6.24 +  in subst_operation overloading end;
    6.25 +
    6.26  fun term_check ts lthy =
    6.27    let
    6.28      val overloading = get_overloading lthy;
    6.29 -    fun subst (t as Const (c, ty)) = (case AList.lookup (op =) overloading (c, ty)
    6.30 -         of SOME (v, _) => Free (v, ty)
    6.31 -          | NONE => t)
    6.32 -      | subst t = t;
    6.33 -    val ts' = (map o map_aterms) subst ts;
    6.34 +    val ts' = map (subst_operation overloading) ts;
    6.35    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
    6.36  
    6.37  fun term_uncheck ts lthy =