src/Pure/Isar/code.ML
changeset 24423 ae9cd0e92423
parent 24283 8ca96f4e49cd
child 24585 c359896d0f48
     1.1 --- a/src/Pure/Isar/code.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  sig
     1.5    val add_func: bool -> thm -> theory -> theory
     1.6    val del_func: thm -> theory -> theory
     1.7 -  val add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory
     1.8 +  val add_funcl: string * thm list Susp.T -> theory -> theory
     1.9    val add_func_attr: bool -> Attrib.src
    1.10    val add_inline: thm -> theory -> theory
    1.11    val del_inline: thm -> theory -> theory
    1.12 @@ -20,17 +20,15 @@
    1.13    val del_preproc: string -> theory -> theory
    1.14    val add_post: thm -> theory -> theory
    1.15    val del_post: thm -> theory -> theory
    1.16 -  val add_datatype: string * ((string * sort) list * (string * typ list) list)
    1.17 -    -> theory -> theory
    1.18 -  val add_datatype_consts: CodeUnit.const list -> theory -> theory
    1.19 -  val add_datatype_consts_cmd: string list -> theory -> theory
    1.20 +  val add_datatype: (string * typ) list -> theory -> theory
    1.21 +  val add_datatype_cmd: string list -> theory -> theory
    1.22  
    1.23    val coregular_algebra: theory -> Sorts.algebra
    1.24    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
    1.25 -  val these_funcs: theory -> CodeUnit.const -> thm list
    1.26 +  val these_funcs: theory -> string -> thm list
    1.27    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    1.28 -  val get_datatype_of_constr: theory -> CodeUnit.const -> string option
    1.29 -  val default_typ: theory -> CodeUnit.const -> typ
    1.30 +  val get_datatype_of_constr: theory -> string -> string option
    1.31 +  val default_typ: theory -> string -> typ
    1.32  
    1.33    val preprocess_conv: cterm -> thm
    1.34    val postprocess_conv: cterm -> thm
    1.35 @@ -45,7 +43,7 @@
    1.36    type T
    1.37    val empty: T
    1.38    val merge: Pretty.pp -> T * T -> T
    1.39 -  val purge: theory option -> CodeUnit.const list option -> T -> T
    1.40 +  val purge: theory option -> string list option -> T -> T
    1.41  end;
    1.42  
    1.43  signature CODE_DATA =
    1.44 @@ -60,7 +58,7 @@
    1.45  sig
    1.46    include CODE
    1.47    val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
    1.48 -    -> (theory option -> CodeUnit.const list option -> Object.T -> Object.T) -> serial
    1.49 +    -> (theory option -> string list option -> Object.T -> Object.T) -> serial
    1.50    val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.51      -> theory -> 'a
    1.52    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.53 @@ -74,9 +72,6 @@
    1.54  
    1.55  (** preliminaries **)
    1.56  
    1.57 -structure Consttab = CodeUnit.Consttab;
    1.58 -
    1.59 -
    1.60  (* certificate theorems *)
    1.61  
    1.62  fun string_of_lthms r = case Susp.peek r
    1.63 @@ -224,24 +219,23 @@
    1.64  
    1.65  fun join_func_thms (tabs as (tab1, tab2)) =
    1.66    let
    1.67 -    val cs1 = Consttab.keys tab1;
    1.68 -    val cs2 = Consttab.keys tab2;
    1.69 -    val cs' = filter (member CodeUnit.eq_const cs2) cs1;
    1.70 +    val cs1 = Symtab.keys tab1;
    1.71 +    val cs2 = Symtab.keys tab2;
    1.72 +    val cs' = filter (member (op =) cs2) cs1;
    1.73      val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
    1.74 -    val cs''' = ref [] : CodeUnit.const list ref;
    1.75 +    val cs''' = ref [] : string list ref;
    1.76      fun merge c x = let val (touched, thms') = merge_sdthms x in
    1.77        (if touched then cs''' := cons c (!cs''') else (); thms') end;
    1.78 -  in (cs'' @ !cs''', Consttab.join merge tabs) end;
    1.79 +  in (cs'' @ !cs''', Symtab.join merge tabs) end;
    1.80  fun merge_funcs (thms1, thms2) =
    1.81    let
    1.82      val (consts, thms) = join_func_thms (thms1, thms2);
    1.83    in (SOME consts, thms) end;
    1.84  
    1.85  val eq_string = op = : string * string -> bool;
    1.86 -val eq_co = op = : (string * typ list) * (string * typ list) -> bool;
    1.87  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
    1.88    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
    1.89 -    andalso gen_eq_set eq_co (cs1, cs2);
    1.90 +    andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
    1.91  fun merge_dtyps (tabs as (tab1, tab2)) =
    1.92    let
    1.93      val tycos1 = Symtab.keys tab1;
    1.94 @@ -256,7 +250,7 @@
    1.95    in ((new_types, diff_types), Symtab.join join tabs) end;
    1.96  
    1.97  datatype spec = Spec of {
    1.98 -  funcs: sdthms Consttab.table,
    1.99 +  funcs: sdthms Symtab.table,
   1.100    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
   1.101  };
   1.102  
   1.103 @@ -289,7 +283,7 @@
   1.104      val touched = if touched' then NONE else touched_cs;
   1.105    in (touched, mk_exec (thmproc, spec)) end;
   1.106  val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   1.107 -  mk_spec (Consttab.empty, Symtab.empty));
   1.108 +  mk_spec (Symtab.empty, Symtab.empty));
   1.109  
   1.110  fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
   1.111  fun the_spec (Exec { spec = Spec x, ...}) = x;
   1.112 @@ -310,7 +304,7 @@
   1.113  type kind = {
   1.114    empty: Object.T,
   1.115    merge: Pretty.pp -> Object.T * Object.T -> Object.T,
   1.116 -  purge: theory option -> CodeUnit.const list option -> Object.T -> Object.T
   1.117 +  purge: theory option -> string list option -> Object.T -> Object.T
   1.118  };
   1.119  
   1.120  val kinds = ref (Datatab.empty: kind Datatab.table);
   1.121 @@ -429,13 +423,14 @@
   1.122              :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
   1.123                   | (c, tys) =>
   1.124                       (Pretty.block o Pretty.breaks)
   1.125 -                        (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
   1.126 +                        (Pretty.str (CodeUnit.string_of_const thy c)
   1.127 +                          :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
   1.128            );
   1.129      val inlines = (#inlines o the_thmproc) exec;
   1.130      val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
   1.131      val preprocs = (map fst o #preprocs o the_thmproc) exec;
   1.132      val funs = the_funcs exec
   1.133 -      |> Consttab.dest
   1.134 +      |> Symtab.dest
   1.135        |> (map o apfst) (CodeUnit.string_of_const thy)
   1.136        |> sort (string_ord o pairself fst);
   1.137      val dtyps = the_dtyps exec
   1.138 @@ -499,9 +494,11 @@
   1.139            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   1.140        in map (Thm.instantiate (instT, [])) thms' end;
   1.141  
   1.142 +fun const_of_func thy = Class.unoverload_const thy o CodeUnit.head_func;
   1.143 +
   1.144  fun certify_const thy const thms =
   1.145    let
   1.146 -    fun cert thm = if CodeUnit.eq_const (const, fst (CodeUnit.head_func thm))
   1.147 +    fun cert thm = if const = const_of_func thy thm
   1.148        then thm else error ("Wrong head of defining equation,\nexpected constant "
   1.149          ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
   1.150    in map cert thms end;
   1.151 @@ -527,15 +524,17 @@
   1.152  fun specific_constraints thy (class, tyco) =
   1.153    let
   1.154      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
   1.155 -    val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
   1.156 +    val clsops = (map fst o these o Option.map snd
   1.157 +      o try (AxClass.params_of_class thy)) class;
   1.158      val funcs = clsops
   1.159 -      |> map (fn (clsop, _) => (clsop, SOME tyco))
   1.160 -      |> map (Consttab.lookup ((the_funcs o get_exec) thy))
   1.161 +      |> map (fn c => Class.inst_const thy (c, tyco))
   1.162 +      |> map (Symtab.lookup ((the_funcs o get_exec) thy))
   1.163        |> (map o Option.map) (Susp.force o fst)
   1.164        |> maps these
   1.165 -      |> map (Thm.transfer thy);
   1.166 -    val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
   1.167 -      o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodeUnit.head_func) funcs;
   1.168 +      |> map (Thm.transfer thy)
   1.169 +    fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   1.170 +      | sorts_of tys = map (snd o dest_TVar) tys;
   1.171 +    val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
   1.172    in sorts end;
   1.173  
   1.174  fun weakest_constraints thy (class, tyco) =
   1.175 @@ -587,8 +586,9 @@
   1.176  fun assert_func_typ thm =
   1.177    let
   1.178      val thy = Thm.theory_of_thm thm;
   1.179 -    fun check_typ_classop class (const as (c, SOME tyco), thm) =
   1.180 +    fun check_typ_classop tyco (c, thm) =
   1.181            let
   1.182 +            val SOME class = AxClass.class_of_param thy c;
   1.183              val (_, ty) = CodeUnit.head_func thm;
   1.184              val ty_decl = classop_weakest_typ thy class (c, tyco);
   1.185              val ty_strongest = classop_strongest_typ thy class (c, tyco);
   1.186 @@ -615,12 +615,8 @@
   1.187                ^ string_of_thm thm
   1.188                ^ "\nis incompatible with permitted least general type\n"
   1.189                ^ CodeUnit.string_of_typ thy ty_strongest)
   1.190 -          end
   1.191 -      | check_typ_classop class ((c, NONE), thm) =
   1.192 -          CodeUnit.bad_thm ("Illegal type for class operation " ^ quote c
   1.193 -           ^ "\nin defining equation\n"
   1.194 -           ^ string_of_thm thm);
   1.195 -    fun check_typ_fun (const as (c, _), thm) =
   1.196 +          end;
   1.197 +    fun check_typ_fun (c, thm) =
   1.198        let
   1.199          val (_, ty) = CodeUnit.head_func thm;
   1.200          val ty_decl = Sign.the_const_type thy c;
   1.201 @@ -632,11 +628,11 @@
   1.202             ^ "\nis incompatible with declared function type\n"
   1.203             ^ CodeUnit.string_of_typ thy ty_decl)
   1.204        end;
   1.205 -    fun check_typ (const as (c, _), thm) =
   1.206 -      case AxClass.class_of_param thy c
   1.207 -       of SOME class => check_typ_classop class (const, thm)
   1.208 -        | NONE => check_typ_fun (const, thm);
   1.209 -  in check_typ (fst (CodeUnit.head_func thm), thm) end;
   1.210 +    fun check_typ (c, thm) =
   1.211 +      case Class.param_const thy c
   1.212 +       of SOME (c, tyco) => check_typ_classop tyco (c, thm)
   1.213 +        | NONE => check_typ_fun (c, thm);
   1.214 +  in check_typ (const_of_func thy thm, thm) end;
   1.215  
   1.216  val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
   1.217  val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
   1.218 @@ -647,21 +643,56 @@
   1.219  
   1.220  (** interfaces and attributes **)
   1.221  
   1.222 +fun get_datatype thy tyco =
   1.223 +  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.224 +   of SOME spec => spec
   1.225 +    | NONE => Sign.arity_number thy tyco
   1.226 +        |> Name.invents Name.context "'a"
   1.227 +        |> map (rpair [])
   1.228 +        |> rpair [];
   1.229 +
   1.230 +fun get_datatype_of_constr thy c =
   1.231 +  case (snd o strip_type o Sign.the_const_type thy) c
   1.232 +   of Type (tyco, _) => if member (op =)
   1.233 +       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
   1.234 +       then SOME tyco else NONE
   1.235 +    | _ => NONE;
   1.236 +
   1.237 +fun get_constr_typ thy c =
   1.238 +  case get_datatype_of_constr thy c
   1.239 +   of SOME tyco => let
   1.240 +          val (vs, cos) = get_datatype thy tyco;
   1.241 +          val SOME tys = AList.lookup (op =) cos c;
   1.242 +          val ty = tys ---> Type (tyco, map TFree vs);
   1.243 +        in SOME (Logic.varifyT ty) end
   1.244 +    | NONE => NONE;
   1.245 +
   1.246  fun add_func true thm thy =
   1.247        let
   1.248          val func = mk_func thm;
   1.249 -        val (const, _) = CodeUnit.head_func func;
   1.250 -      in map_exec_purge (SOME [const]) (map_funcs
   1.251 -        (Consttab.map_default
   1.252 -          (const, (Susp.value [], [])) (add_thm func))) thy
   1.253 +        val c = const_of_func thy func;
   1.254 +        val _ = if (is_some o AxClass.class_of_param thy) c
   1.255 +          then error ("Rejected polymorphic equation for overloaded constant:\n"
   1.256 +            ^ string_of_thm thm)
   1.257 +          else ();
   1.258 +        val _ = if (is_some o get_datatype_of_constr thy) c
   1.259 +          then error ("Rejected equation for datatype constructor:\n"
   1.260 +            ^ string_of_thm func)
   1.261 +          else ();
   1.262 +      in map_exec_purge (SOME [c]) (map_funcs
   1.263 +        (Symtab.map_default
   1.264 +          (c, (Susp.value [], [])) (add_thm func))) thy
   1.265        end
   1.266    | add_func false thm thy =
   1.267        case mk_func_liberal thm
   1.268         of SOME func => let
   1.269 -              val (const, _) = CodeUnit.head_func func
   1.270 -            in map_exec_purge (SOME [const]) (map_funcs
   1.271 -              (Consttab.map_default
   1.272 -                (const, (Susp.value [], [])) (add_thm func))) thy
   1.273 +              val c = const_of_func thy func
   1.274 +            in if (is_some o AxClass.class_of_param thy) c
   1.275 +              orelse (is_some o get_datatype_of_constr thy) c
   1.276 +              then thy
   1.277 +              else map_exec_purge (SOME [c]) (map_funcs
   1.278 +              (Symtab.map_default
   1.279 +                (c, (Susp.value [], [])) (add_thm func))) thy
   1.280              end
   1.281          | NONE => thy;
   1.282  
   1.283 @@ -672,9 +703,9 @@
   1.284  fun del_func thm thy =
   1.285    let
   1.286      val func = mk_func thm;
   1.287 -    val (const, _) = CodeUnit.head_func func;
   1.288 +    val const = const_of_func thy func;
   1.289    in map_exec_purge (SOME [const]) (map_funcs
   1.290 -    (Consttab.map_entry
   1.291 +    (Symtab.map_entry
   1.292        const (del_thm func))) thy
   1.293    end;
   1.294  
   1.295 @@ -684,41 +715,31 @@
   1.296        (*FIXME must check compatibility with sort algebra;
   1.297          alas, naive checking results in non-termination!*)
   1.298    in
   1.299 -    map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
   1.300 +    map_exec_purge (SOME [const]) (map_funcs (Symtab.map_default (const, (Susp.value [], []))
   1.301        (add_lthms lthms'))) thy
   1.302    end;
   1.303  
   1.304  fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
   1.305    (fn thm => Context.mapping (add_func strict thm) I));
   1.306  
   1.307 -local
   1.308 -
   1.309 -fun del_datatype tyco thy =
   1.310 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.311 -   of SOME (vs, cos) => let
   1.312 -        val consts = CodeUnit.consts_of_cos thy tyco vs cos;
   1.313 -      in map_exec_purge (if null consts then NONE else SOME consts)
   1.314 -        (map_dtyps (Symtab.delete tyco)) thy end
   1.315 -    | NONE => thy;
   1.316 -
   1.317 -in
   1.318 -
   1.319 -fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
   1.320 +fun add_datatype raw_cs thy =
   1.321    let
   1.322 -    val consts = CodeUnit.consts_of_cos thy tyco vs cos;
   1.323 +    val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
   1.324 +    val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
   1.325 +    val purge_cs = map fst (snd vs_cos);
   1.326 +    val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.327 +     of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
   1.328 +      | NONE => NONE;
   1.329    in
   1.330      thy
   1.331 -    |> del_datatype tyco
   1.332 -    |> map_exec_purge (SOME consts) (map_dtyps (Symtab.update_new (tyco, vs_cos)))
   1.333 +    |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
   1.334 +        #> map_funcs (fold (Symtab.delete_safe o fst) cs))
   1.335    end;
   1.336  
   1.337 -fun add_datatype_consts consts thy =
   1.338 -  add_datatype (CodeUnit.cos_of_consts thy consts) thy;
   1.339 -
   1.340 -fun add_datatype_consts_cmd raw_cs thy =
   1.341 -  add_datatype_consts (map (CodeUnit.read_const thy) raw_cs) thy
   1.342 -
   1.343 -end; (*local*)
   1.344 +fun add_datatype_cmd raw_cs thy =
   1.345 +  let
   1.346 +    val cs = map (CodeUnit.read_bare_const thy) raw_cs;
   1.347 +  in add_datatype cs thy end;
   1.348  
   1.349  fun add_inline thm thy =
   1.350    (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   1.351 @@ -790,7 +811,7 @@
   1.352  fun apply_preproc thy f [] = []
   1.353    | apply_preproc thy f (thms as (thm :: _)) =
   1.354        let
   1.355 -        val (const, _) = CodeUnit.head_func thm;
   1.356 +        val const = const_of_func thy thm;
   1.357          val thms' = f thy thms;
   1.358        in certify_const thy const thms' end;
   1.359  
   1.360 @@ -807,7 +828,8 @@
   1.361    |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
   1.362    |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
   1.363  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   1.364 -  |> common_typ_funcs;
   1.365 +  |> common_typ_funcs
   1.366 +  |> map (Conv.fconv_rule (Class.unoverload thy));
   1.367  
   1.368  fun preprocess_conv ct =
   1.369    let
   1.370 @@ -817,6 +839,7 @@
   1.371      |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
   1.372      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
   1.373          ((#inline_procs o the_thmproc o get_exec) thy)
   1.374 +    |> rhs_conv (Class.unoverload thy)
   1.375    end;
   1.376  
   1.377  fun postprocess_conv ct =
   1.378 @@ -824,49 +847,24 @@
   1.379      val thy = Thm.theory_of_cterm ct;
   1.380    in
   1.381      ct
   1.382 -    |> MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)
   1.383 +    |> Class.overload thy
   1.384 +    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
   1.385    end;
   1.386  
   1.387  end; (*local*)
   1.388  
   1.389 -fun get_datatype thy tyco =
   1.390 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.391 -   of SOME spec => spec
   1.392 -    | NONE => Sign.arity_number thy tyco
   1.393 -        |> Name.invents Name.context "'a"
   1.394 -        |> map (rpair [])
   1.395 -        |> rpair [];
   1.396 -
   1.397 -fun get_datatype_of_constr thy const =
   1.398 -  case CodeUnit.co_of_const' thy const
   1.399 -   of SOME (tyco, (_, co)) => if member eq_co
   1.400 -        (Symtab.lookup (((the_dtyps o get_exec) thy)) tyco
   1.401 -          |> Option.map snd
   1.402 -          |> the_default []) co then SOME tyco else NONE
   1.403 -    | NONE => NONE;
   1.404 -
   1.405 -fun get_constr_typ thy const =
   1.406 -  case get_datatype_of_constr thy const
   1.407 -   of SOME tyco => let
   1.408 -        val (vs, cos) = get_datatype thy tyco;
   1.409 -        val (_, (_, (co, tys))) = CodeUnit.co_of_const thy const
   1.410 -      in (tys ---> Type (tyco, map TFree vs))
   1.411 -        |> map_atyps (fn TFree (v, _) => TFree (v, AList.lookup (op =) vs v |> the))
   1.412 -        |> Logic.varifyT
   1.413 -        |> SOME end
   1.414 -    | NONE => NONE;
   1.415 -
   1.416 -fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
   1.417 -      ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
   1.418 -  | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
   1.419 -       of SOME class => SOME (Term.map_type_tvar
   1.420 -            (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
   1.421 -        | NONE => get_constr_typ thy const;
   1.422 +fun default_typ_proto thy c = case Class.param_const thy c
   1.423 + of SOME (c, tyco) => classop_weakest_typ thy ((the o AxClass.class_of_param thy) c)
   1.424 +      (c, tyco) |> SOME
   1.425 +  | NONE => (case AxClass.class_of_param thy c
   1.426 +     of SOME class => SOME (Term.map_type_tvar
   1.427 +          (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
   1.428 +      | NONE => get_constr_typ thy c);
   1.429  
   1.430  local
   1.431  
   1.432  fun get_funcs thy const =
   1.433 -  Consttab.lookup ((the_funcs o get_exec) thy) const
   1.434 +  Symtab.lookup ((the_funcs o get_exec) thy) const
   1.435    |> Option.map (Susp.force o fst)
   1.436    |> these
   1.437    |> map (Thm.transfer thy);
   1.438 @@ -883,10 +881,10 @@
   1.439      |> drop_refl thy
   1.440    end;
   1.441  
   1.442 -fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
   1.443 +fun default_typ thy c = case default_typ_proto thy c
   1.444   of SOME ty => ty
   1.445 -  | NONE => (case get_funcs thy const
   1.446 -     of thm :: _ => snd (CodeUnit.head_func thm)
   1.447 +  | NONE => (case get_funcs thy c
   1.448 +     of thm :: _ => snd (CodeUnit.head_func (Conv.fconv_rule (Class.unoverload thy) thm))
   1.449        | [] => Sign.the_const_type thy c);
   1.450  
   1.451  end; (*local*)