explicit type variables for instantiation
authorhaftmann
Tue Jan 08 11:37:30 2008 +0100 (2008-01-08)
changeset 2586411f531354852
parent 25863 5b4a8b1d0f88
child 25865 a141d6bfd398
explicit type variables for instantiation
src/HOL/Library/Eval.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Tue Jan 08 11:37:29 2008 +0100
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Jan 08 11:37:30 2008 +0100
     1.3 @@ -99,10 +99,11 @@
     1.4    fun interpretator tyco thy =
     1.5      let
     1.6        val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
     1.7 -      val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
     1.8 +      val vs = Name.names Name.context "'a" sorts;
     1.9 +      val ty = Type (tyco, map TFree vs);
    1.10      in
    1.11        thy
    1.12 -      |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
    1.13 +      |> TheoryTarget.instantiation ([tyco], vs, @{sort typ_of})
    1.14        |> define_typ_of ty
    1.15        |> snd
    1.16        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.17 @@ -265,7 +266,7 @@
    1.18        val defs = map (mk_terms_of_defs vs) css;
    1.19      in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
    1.20          andalso not (tycos = [@{type_name typ}])
    1.21 -      then SOME (sorts, defs)
    1.22 +      then SOME (vs, defs)
    1.23        else NONE
    1.24      end;
    1.25    fun prep' ctxt proto_eqs =
    1.26 @@ -279,9 +280,9 @@
    1.27        val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs);
    1.28      in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end;
    1.29    fun interpretator tycos thy = case prep thy tycos
    1.30 -   of SOME (sorts, defs) =>
    1.31 +   of SOME (vs, defs) =>
    1.32        thy
    1.33 -      |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
    1.34 +      |> TheoryTarget.instantiation (tycos, vs, @{sort term_of})
    1.35        |> primrec defs
    1.36        |> snd
    1.37        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jan 08 11:37:29 2008 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jan 08 11:37:30 2008 +0100
     2.3 @@ -431,11 +431,11 @@
     2.4        in
     2.5          Code.add_funcl (const, Susp.delay get_thms) thy
     2.6        end;
     2.7 -    val sorts_eq =
     2.8 -      map (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq] o snd) vs;
     2.9 +    val vs' = (map o apsnd)
    2.10 +      (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
    2.11    in
    2.12      thy
    2.13 -    |> TheoryTarget.instantiation (dtcos, sorts_eq, [HOLogic.class_eq])
    2.14 +    |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
    2.15      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    2.16      |> LocalTheory.exit
    2.17      |> ProofContext.theory_of
     3.1 --- a/src/HOL/Tools/function_package/size.ML	Tue Jan 08 11:37:29 2008 +0100
     3.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Jan 08 11:37:30 2008 +0100
     3.3 @@ -60,23 +60,23 @@
     3.4  
     3.5  fun prove_size_thms (info : datatype_info) new_type_names thy =
     3.6    let
     3.7 -    val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
     3.8 +    val {descr, alt_names, sorts = raw_sorts, rec_names, rec_rewrites, induction, ...} = info;
     3.9  
    3.10      (*normalize type variable names to accomodate policy imposed by instantiation target*)
    3.11 -    val tvars = (map dest_TFree o snd o dest_Type o hd) (get_rec_types descr sorts)
    3.12 -      ~~ Name.invents Name.context Name.aT (length sorts);
    3.13 -    val norm_tvars = map_atyps
    3.14 -      (fn TFree (v, sort) => TFree (the (AList.lookup (op =) tvars v), sort));
    3.15 +    val tvars = (map dest_TFree o snd o dest_Type o hd) (get_rec_types descr raw_sorts)
    3.16 +      ~~ Name.invents Name.context Name.aT (length raw_sorts);
    3.17 +    val sorts = tvars
    3.18 +      |> map (fn (v, _) => (v, the (AList.lookup (op =) raw_sorts v)));
    3.19  
    3.20      val l = length new_type_names;
    3.21      val alt_names' = (case alt_names of
    3.22        NONE => replicate l NONE | SOME names => map SOME names);
    3.23      val descr' = List.take (descr, l);
    3.24      val (rec_names1, rec_names2) = chop l rec_names;
    3.25 -    val recTs = map norm_tvars (get_rec_types descr sorts);
    3.26 +    val recTs = get_rec_types descr sorts;
    3.27      val (recTs1, recTs2) = chop l recTs;
    3.28      val (_, (_, paramdts, _)) :: _ = descr;
    3.29 -    val paramTs = map (norm_tvars o typ_of_dtyp descr sorts) paramdts;
    3.30 +    val paramTs = map (typ_of_dtyp descr sorts) paramdts;
    3.31      val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
    3.32        map (fn T as TFree (s, _) =>
    3.33          let
    3.34 @@ -108,7 +108,7 @@
    3.35      (* instantiation for primrec combinator *)
    3.36      fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
    3.37        let
    3.38 -        val Ts = map (norm_tvars o typ_of_dtyp descr sorts) cargs;
    3.39 +        val Ts = map (typ_of_dtyp descr sorts) cargs;
    3.40          val k = length (filter is_rec_type cargs);
    3.41          val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
    3.42            if is_rec_type dt then (Bound i :: us, i + 1, j + 1)
    3.43 @@ -139,18 +139,12 @@
    3.44      fun define_overloaded (def_name, eq) lthy =
    3.45        let
    3.46          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
    3.47 -        val (thm, lthy') = lthy
    3.48 +        val ((_, (_, thm)), lthy') = lthy
    3.49            |> LocalTheory.define Thm.definitionK ((c, NoSyn), ((def_name, []), rhs));
    3.50          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
    3.51 -        val thm' = thm
    3.52 -          |> Assumption.export false lthy' ctxt_thy o snd o snd
    3.53 -          |> singleton (Variable.export lthy' ctxt_thy)
    3.54 +        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    3.55        in (thm', lthy') end;
    3.56  
    3.57 -    val size_sorts = tvars
    3.58 -      |> map (fn (v, _) => Sorts.inter_sort (Sign.classes_of thy) (HOLogic.typeS,
    3.59 -           the (AList.lookup (op =) sorts v)));
    3.60 -
    3.61      val ((size_def_thms, size_def_thms'), thy') =
    3.62        thy
    3.63        |> Sign.add_consts_i (map (fn (s, T) =>
    3.64 @@ -160,7 +154,7 @@
    3.65          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
    3.66             (def_names ~~ (size_fns ~~ rec_combs1)))
    3.67        ||> TheoryTarget.instantiation
    3.68 -           (map (#1 o snd) descr', size_sorts, [HOLogic.class_size])
    3.69 +           (map (#1 o snd) descr', sorts, [HOLogic.class_size])
    3.70        ||>> fold_map define_overloaded
    3.71          (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
    3.72        ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    3.73 @@ -192,7 +186,7 @@
    3.74      (* characteristic equations for size functions *)
    3.75      fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
    3.76        let
    3.77 -        val Ts = map (norm_tvars o typ_of_dtyp descr sorts) cargs;
    3.78 +        val Ts = map (typ_of_dtyp descr sorts) cargs;
    3.79          val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
    3.80          val ts = List.mapPartial (fn (sT as (s, T), dt) =>
    3.81            Option.map (fn sz => sz $ Free sT)
     4.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Jan 08 11:37:29 2008 +0100
     4.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Jan 08 11:37:30 2008 +0100
     4.3 @@ -124,14 +124,13 @@
     4.4  fun add_typecopy_spec tyco thy =
     4.5    let
     4.6      val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
     4.7 -    val sorts_eq =
     4.8 -      map (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq] o snd) vs;
     4.9 +    val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
    4.10      val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
    4.11    in
    4.12      thy
    4.13      |> Code.add_datatype [(constr, ty)]
    4.14      |> Code.add_func proj_def
    4.15 -    |> TheoryTarget.instantiation ([tyco], sorts_eq, [HOLogic.class_eq])
    4.16 +    |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
    4.17      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    4.18      |> LocalTheory.exit
    4.19      |> ProofContext.theory_of
     5.1 --- a/src/Pure/Isar/class.ML	Tue Jan 08 11:37:29 2008 +0100
     5.2 +++ b/src/Pure/Isar/class.ML	Tue Jan 08 11:37:30 2008 +0100
     5.3 @@ -30,7 +30,7 @@
     5.4    val print_classes: theory -> unit
     5.5  
     5.6    (*instances*)
     5.7 -  val init_instantiation: string list * sort list * sort -> theory -> local_theory
     5.8 +  val init_instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     5.9    val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    5.10    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    5.11    val conclude_instantiation: local_theory -> local_theory
    5.12 @@ -681,7 +681,7 @@
    5.13  (* bookkeeping *)
    5.14  
    5.15  datatype instantiation = Instantiation of {
    5.16 -  arities: string list * sort list * sort,
    5.17 +  arities: string list * (string * sort) list * sort,
    5.18    params: ((string * string) * (string * typ)) list
    5.19      (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
    5.20  }
    5.21 @@ -768,25 +768,24 @@
    5.22      explode #> scan_valids #> implode
    5.23    end;
    5.24  
    5.25 -fun init_instantiation (tycos, sorts, sort) thy =
    5.26 +fun init_instantiation (tycos, vs, sort) thy =
    5.27    let
    5.28      val _ = if null tycos then error "At least one arity must be given" else ();
    5.29      val _ = map (the_class_data thy) sort;
    5.30 -    val vs = map TFree (Name.names Name.context Name.aT sorts);
    5.31      fun type_name "*" = "prod"
    5.32        | type_name "+" = "sum"
    5.33        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
    5.34      fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
    5.35        then NONE else SOME ((c, tyco),
    5.36 -        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
    5.37 +        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
    5.38      val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    5.39    in
    5.40      thy
    5.41      |> ProofContext.init
    5.42 -    |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
    5.43 -    |> fold (Variable.declare_term o Logic.mk_type) vs
    5.44 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    5.45 +    |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
    5.46      |> fold (Variable.declare_names o Free o snd) params
    5.47 -    |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
    5.48 +    |> fold (fn tyco => ProofContext.add_arity (tyco, map snd vs, sort)) tycos
    5.49      |> Context.proof_map (
    5.50          Syntax.add_term_check 0 "instance" inst_term_check
    5.51          #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
    5.52 @@ -794,8 +793,8 @@
    5.53  
    5.54  fun gen_instantiation_instance do_proof after_qed lthy =
    5.55    let
    5.56 -    val (tycos, sorts, sort) = (#arities o the_instantiation) lthy;
    5.57 -    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    5.58 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    5.59 +    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    5.60      fun after_qed' results =
    5.61        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
    5.62        #> after_qed;
    5.63 @@ -814,10 +813,10 @@
    5.64  fun conclude_instantiation lthy =
    5.65    let
    5.66      val { arities, params } = the_instantiation lthy;
    5.67 -    val (tycos, sorts, sort) = arities;
    5.68 +    val (tycos, vs, sort) = arities;
    5.69      val thy = ProofContext.theory_of lthy;
    5.70      val _ = map (fn tyco => if Sign.of_sort thy
    5.71 -        (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
    5.72 +        (Type (tyco, map TFree vs), sort)
    5.73        then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
    5.74          tycos;
    5.75      (*this checkpoint should move to AxClass as soon as "attach" has disappeared*)
    5.76 @@ -830,12 +829,12 @@
    5.77  fun pretty_instantiation lthy =
    5.78    let
    5.79      val { arities, params } = the_instantiation lthy;
    5.80 -    val (tycos, sorts, sort) = arities;
    5.81 +    val (tycos, vs, sort) = arities;
    5.82      val thy = ProofContext.theory_of lthy;
    5.83 -    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, sorts, sort);
    5.84 +    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    5.85      fun pr_param ((c, _), (v, ty)) =
    5.86 -      (Pretty.block o Pretty.breaks) [(Pretty.str o Sign.extern_const thy) c, Pretty.str "::",
    5.87 -        Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
    5.88 +      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    5.89 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
    5.90    in
    5.91      (Pretty.block o Pretty.fbreaks)
    5.92        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
     6.1 --- a/src/Pure/Isar/instance.ML	Tue Jan 08 11:37:29 2008 +0100
     6.2 +++ b/src/Pure/Isar/instance.ML	Tue Jan 08 11:37:30 2008 +0100
     6.3 @@ -15,32 +15,31 @@
     6.4  structure Instance : INSTANCE =
     6.5  struct
     6.6  
     6.7 +fun read_single_arity thy (raw_tyco, raw_sorts, raw_sort) =
     6.8 +  let
     6.9 +    val (tyco, sorts, sort) = Sign.read_arity thy (raw_tyco, raw_sorts, raw_sort);
    6.10 +    val vs = Name.names Name.context Name.aT sorts;
    6.11 +  in (tyco, vs, sort) end;
    6.12 +
    6.13  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    6.14    let
    6.15      val all_arities = map (fn raw_tyco => Sign.read_arity thy
    6.16        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    6.17      val tycos = map #1 all_arities;
    6.18      val (_, sorts, sort) = hd all_arities;
    6.19 -  in (tycos, sorts, sort) end;
    6.20 +    val vs = Name.names Name.context Name.aT sorts;
    6.21 +  in (tycos, vs, sort) end;
    6.22  
    6.23  fun instantiation_cmd raw_arities thy =
    6.24    TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
    6.25  
    6.26 -fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
    6.27 +fun instance_cmd raw_arities defs thy =
    6.28    let
    6.29 -    val (tyco, sorts, sort) = prep_arity thy raw_arities;
    6.30 -    fun export_defs ctxt = 
    6.31 -      let
    6.32 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
    6.33 -      in
    6.34 -        map (snd o snd)
    6.35 -        #> map (Assumption.export false ctxt ctxt_thy)
    6.36 -        #> Variable.export ctxt ctxt_thy
    6.37 -      end;
    6.38 +    val (tyco, vs, sort) = read_single_arity thy raw_arities;
    6.39      fun mk_def ctxt ((name, raw_attr), raw_t) =
    6.40        let
    6.41 -        val attr = map (prep_attr thy) raw_attr;
    6.42 -        val t = parse_term ctxt raw_t;
    6.43 +        val attr = map (Attrib.intern_src thy) raw_attr;
    6.44 +        val t = Syntax.parse_prop ctxt raw_t;
    6.45        in (NONE, ((name, attr), t)) end;
    6.46      fun define def ctxt =
    6.47        let
    6.48 @@ -51,18 +50,15 @@
    6.49    in if not (null defs) orelse forall (Class.is_class thy) sort
    6.50    then
    6.51      thy
    6.52 -    |> TheoryTarget.instantiation ([tyco], sorts, sort)
    6.53 +    |> TheoryTarget.instantiation ([tyco], vs, sort)
    6.54      |> `(fn ctxt => map (mk_def ctxt) defs)
    6.55      |-> (fn defs => fold_map Specification.definition defs)
    6.56 -    |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
    6.57 -    ||> LocalTheory.reinit
    6.58 -    |-> (fn defs => do_proof defs)
    6.59 +    |> snd
    6.60 +    |> LocalTheory.reinit
    6.61 +    |> Class.instantiation_instance Class.conclude_instantiation
    6.62    else
    6.63      thy
    6.64 -    |> do_proof' (tyco, sorts, sort)
    6.65 +    |> Class.instance_arity I (tyco, map snd vs, sort)
    6.66    end;
    6.67  
    6.68 -val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
    6.69 -  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
    6.70 -
    6.71  end;
     7.1 --- a/src/Pure/Isar/theory_target.ML	Tue Jan 08 11:37:29 2008 +0100
     7.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Jan 08 11:37:30 2008 +0100
     7.3 @@ -8,14 +8,14 @@
     7.4  signature THEORY_TARGET =
     7.5  sig
     7.6    val peek: local_theory -> {target: string, is_locale: bool,
     7.7 -    is_class: bool, instantiation: string list * sort list * sort,
     7.8 -    overloading: ((string * typ) * (string * bool)) list}
     7.9 +    is_class: bool, instantiation: string list * (string * sort) list * sort,
    7.10 +    overloading: (string * (string * typ) * bool) list}
    7.11    val init: string option -> theory -> local_theory
    7.12    val begin: string -> Proof.context -> local_theory
    7.13    val context: xstring -> theory -> local_theory
    7.14 -  val instantiation: string list * sort list * sort -> theory -> local_theory
    7.15 -  val overloading: ((string * typ) * (string * bool)) list -> theory -> local_theory
    7.16 -  val overloading_cmd: (((xstring * xstring) * string) * bool) list -> theory -> local_theory
    7.17 +  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    7.18 +  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
    7.19 +  val overloading_cmd: ((xstring * xstring) * bool) list -> theory -> local_theory
    7.20  end;
    7.21  
    7.22  structure TheoryTarget: THEORY_TARGET =
    7.23 @@ -24,8 +24,8 @@
    7.24  (* context data *)
    7.25  
    7.26  datatype target = Target of {target: string, is_locale: bool,
    7.27 -  is_class: bool, instantiation: string list * sort list * sort,
    7.28 -  overloading: ((string * typ) * (string * bool)) list};
    7.29 +  is_class: bool, instantiation: string list * (string * sort) list * sort,
    7.30 +  overloading: (string * (string * typ) * bool) list};
    7.31  
    7.32  fun make_target target is_locale is_class instantiation overloading =
    7.33    Target {target = target, is_locale = is_locale,
    7.34 @@ -366,7 +366,8 @@
    7.35  in
    7.36  
    7.37  fun init target thy = init_lthy_ctxt (init_target thy target) thy;
    7.38 -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
    7.39 +fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt)
    7.40 +  (SOME target)) ctxt;
    7.41  
    7.42  fun context "-" thy = init NONE thy
    7.43    | context target thy = init (SOME (Locale.intern thy target)) thy;
    7.44 @@ -375,18 +376,18 @@
    7.45  
    7.46  fun gen_overloading prep_operation raw_operations thy =
    7.47    let
    7.48 -    val check_const = dest_Const o Syntax.check_term (ProofContext.init thy) o Const;
    7.49 +    val check_const = dest_Const o Syntax.check_term (ProofContext.init thy);
    7.50      val operations = raw_operations
    7.51        |> map (prep_operation thy)
    7.52 -      |> (map o apfst) check_const;
    7.53 +      |> map (fn (v, cTt, checked) => (v, check_const cTt, checked));
    7.54    in
    7.55      thy
    7.56      |> init_lthy_ctxt (init_overloading operations)
    7.57    end;
    7.58  
    7.59 -val overloading = gen_overloading (K I);
    7.60 -val overloading_cmd = gen_overloading (fn thy => fn (((raw_c, rawT), v), checked) =>
    7.61 -  ((Sign.intern_const thy raw_c, Sign.read_typ thy rawT), (v, checked)));
    7.62 +val overloading = gen_overloading (fn _ => fn (v, cT, checked) => (v, Const cT, checked));
    7.63 +val overloading_cmd = gen_overloading (fn thy => fn ((v, raw_cT), checked) =>
    7.64 +  (v, Sign.read_term thy raw_cT, checked));
    7.65  
    7.66  end;
    7.67