tuned interface of structure Code
authorhaftmann
Tue Jul 07 17:21:27 2009 +0200 (2009-07-07)
changeset 31957a9742afd403e
parent 31956 c3844c4d0c2c
child 31958 2133f596c520
tuned interface of structure Code
src/HOL/Tools/recfun_codegen.ML
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Jul 07 17:21:26 2009 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 07 17:21:27 2009 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4          val (thm', _) = Code.mk_eqn thy (K false) (thm, true)
     1.5        in
     1.6          thy
     1.7 -        |> ModuleData.map (Symtab.update (Code.const_eqn thy thm', module_name))
     1.8 +        |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
     1.9          |> Code.add_eqn thm'
    1.10        end;
    1.11  
    1.12 @@ -44,7 +44,7 @@
    1.13  fun expand_eta thy [] = []
    1.14    | expand_eta thy (thms as thm :: _) =
    1.15        let
    1.16 -        val (_, ty) = Code.const_typ_eqn thm;
    1.17 +        val (_, ty) = Code.const_typ_eqn thy thm;
    1.18        in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
    1.19          then thms
    1.20          else map (Code.expand_eta thy 1) thms
     2.1 --- a/src/Pure/Isar/code.ML	Tue Jul 07 17:21:26 2009 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 07 17:21:27 2009 +0200
     2.3 @@ -7,22 +7,18 @@
     2.4  
     2.5  signature CODE =
     2.6  sig
     2.7 +  (*constants*)
     2.8 +  val string_of_const: theory -> string -> string
     2.9 +  val args_number: theory -> string -> int
    2.10 +  val check_const: theory -> term -> string
    2.11 +  val read_bare_const: theory -> string -> string * typ
    2.12 +  val read_const: theory -> string -> string
    2.13 +  val typscheme: theory -> string * typ -> (string * sort) list * typ
    2.14 +
    2.15    (*constructor sets*)
    2.16    val constrset_of_consts: theory -> (string * typ) list
    2.17      -> string * ((string * sort) list * (string * typ list) list)
    2.18  
    2.19 -  (*typ instantiations*)
    2.20 -  val typscheme: theory -> string * typ -> (string * sort) list * typ
    2.21 -  val inst_thm: theory -> sort Vartab.table -> thm -> thm
    2.22 -
    2.23 -  (*constants*)
    2.24 -  val string_of_typ: theory -> typ -> string
    2.25 -  val string_of_const: theory -> string -> string
    2.26 -  val no_args: theory -> string -> int
    2.27 -  val check_const: theory -> term -> string
    2.28 -  val read_bare_const: theory -> string -> string * typ
    2.29 -  val read_const: theory -> string -> string
    2.30 -
    2.31    (*constant aliasses*)
    2.32    val add_const_alias: thm -> theory -> theory
    2.33    val triv_classes: theory -> class list
    2.34 @@ -35,22 +31,12 @@
    2.35    val assert_eqn: theory -> thm * bool -> thm * bool
    2.36    val assert_eqns_const: theory -> string
    2.37      -> (thm * bool) list -> (thm * bool) list
    2.38 -  val const_typ_eqn: thm -> string * typ
    2.39 -  val const_eqn: theory -> thm -> string
    2.40 +  val const_typ_eqn: theory -> thm -> string * typ
    2.41    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
    2.42    val expand_eta: theory -> int -> thm -> thm
    2.43 -  val rewrite_eqn: simpset -> thm -> thm
    2.44 -  val rewrite_head: thm list -> thm -> thm
    2.45    val norm_args: theory -> thm list -> thm list 
    2.46    val norm_varnames: theory -> thm list -> thm list
    2.47  
    2.48 -  (*case certificates*)
    2.49 -  val case_cert: thm -> string * (int * string list)
    2.50 -
    2.51 -  (*infrastructure*)
    2.52 -  val add_attribute: string * attribute parser -> theory -> theory
    2.53 -  val purge_data: theory -> theory
    2.54 -
    2.55    (*executable content*)
    2.56    val add_datatype: (string * typ) list -> theory -> theory
    2.57    val add_datatype_cmd: string list -> theory -> theory
    2.58 @@ -58,25 +44,26 @@
    2.59      (string * ((string * sort) list * (string * typ list) list)
    2.60        -> theory -> theory) -> theory -> theory
    2.61    val add_eqn: thm -> theory -> theory
    2.62 +  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
    2.63    val add_nbe_eqn: thm -> theory -> theory
    2.64    val add_default_eqn: thm -> theory -> theory
    2.65    val add_default_eqn_attribute: attribute
    2.66    val add_default_eqn_attrib: Attrib.src
    2.67    val del_eqn: thm -> theory -> theory
    2.68    val del_eqns: string -> theory -> theory
    2.69 -  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
    2.70    val add_case: thm -> theory -> theory
    2.71    val add_undefined: string -> theory -> theory
    2.72 -
    2.73 -  (*data retrieval*)
    2.74    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    2.75    val get_datatype_of_constr: theory -> string -> string option
    2.76 -  val default_typscheme: theory -> string -> (string * sort) list * typ
    2.77    val these_eqns: theory -> string -> (thm * bool) list
    2.78    val all_eqns: theory -> (thm * bool) list
    2.79    val get_case_scheme: theory -> string -> (int * (int * string list)) option
    2.80    val undefineds: theory -> string list
    2.81    val print_codesetup: theory -> unit
    2.82 +
    2.83 +  (*infrastructure*)
    2.84 +  val add_attribute: string * attribute parser -> theory -> theory
    2.85 +  val purge_data: theory -> theory
    2.86  end;
    2.87  
    2.88  signature CODE_DATA_ARGS =
    2.89 @@ -117,7 +104,7 @@
    2.90   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    2.91    | NONE => Sign.extern_const thy c;
    2.92  
    2.93 -fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
    2.94 +fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
    2.95  
    2.96  
    2.97  (* utilities *)
    2.98 @@ -125,21 +112,7 @@
    2.99  fun typscheme thy (c, ty) =
   2.100    let
   2.101      val ty' = Logic.unvarifyT ty;
   2.102 -    fun dest (TFree (v, sort)) = (v, sort)
   2.103 -      | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty);
   2.104 -    val vs = map dest (Sign.const_typargs thy (c, ty'));
   2.105 -  in (vs, Type.strip_sorts ty') end;
   2.106 -
   2.107 -fun inst_thm thy tvars' thm =
   2.108 -  let
   2.109 -    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
   2.110 -    val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
   2.111 -    fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
   2.112 -     of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
   2.113 -          (tvar, (v, inter_sort (sort, sort'))))
   2.114 -      | NONE => NONE;
   2.115 -    val insts = map_filter mk_inst tvars;
   2.116 -  in Thm.instantiate (insts, []) thm end;
   2.117 +  in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
   2.118  
   2.119  fun expand_eta thy k thm =
   2.120    let
   2.121 @@ -173,23 +146,6 @@
   2.122      |> Conv.fconv_rule Drule.beta_eta_conversion
   2.123    end;
   2.124  
   2.125 -fun eqn_conv conv =
   2.126 -  let
   2.127 -    fun lhs_conv ct = if can Thm.dest_comb ct
   2.128 -      then (Conv.combination_conv lhs_conv conv) ct
   2.129 -      else Conv.all_conv ct;
   2.130 -  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
   2.131 -
   2.132 -fun head_conv conv =
   2.133 -  let
   2.134 -    fun lhs_conv ct = if can Thm.dest_comb ct
   2.135 -      then (Conv.fun_conv lhs_conv) ct
   2.136 -      else conv ct;
   2.137 -  in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
   2.138 -
   2.139 -val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
   2.140 -val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
   2.141 -
   2.142  fun norm_args thy thms =
   2.143    let
   2.144      val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
   2.145 @@ -265,6 +221,19 @@
   2.146    end;
   2.147  
   2.148  
   2.149 +(* reading constants as terms *)
   2.150 +
   2.151 +fun check_bare_const thy t = case try dest_Const t
   2.152 + of SOME c_ty => c_ty
   2.153 +  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   2.154 +
   2.155 +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
   2.156 +
   2.157 +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
   2.158 +
   2.159 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
   2.160 +
   2.161 +
   2.162  (* const aliasses *)
   2.163  
   2.164  structure ConstAlias = TheoryDataFun
   2.165 @@ -280,16 +249,29 @@
   2.166  
   2.167  fun add_const_alias thm thy =
   2.168    let
   2.169 -    val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm)
   2.170 +    val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
   2.171 +     of SOME ofclass_eq => ofclass_eq
   2.172 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.173 +    val (T, class) = case try Logic.dest_of_class ofclass
   2.174 +     of SOME T_class => T_class
   2.175 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.176 +    val tvar = case try Term.dest_TVar T
   2.177 +     of SOME tvar => tvar
   2.178 +      | _ => error ("Bad type: " ^ Display.string_of_thm thm);
   2.179 +    val _ = if Term.add_tvars eqn [] = [tvar] then ()
   2.180 +      else error ("Inconsistent type: " ^ Display.string_of_thm thm);
   2.181 +    val lhs_rhs = case try Logic.dest_equals eqn
   2.182       of SOME lhs_rhs => lhs_rhs
   2.183 -      | _ => error ("Not an equation: " ^ Display.string_of_thm thm);
   2.184 -    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
   2.185 +      | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   2.186 +    val c_c' = case try (pairself (check_const thy)) lhs_rhs
   2.187       of SOME c_c' => c_c'
   2.188 -      | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm);
   2.189 -    val some_class = the_list (AxClass.class_of_param thy (snd c_c'));
   2.190 +      | _ => error ("Not an equation with two constants: "
   2.191 +          ^ Syntax.string_of_term_global thy eqn);
   2.192 +    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
   2.193 +      else error ("Inconsistent class: " ^ Display.string_of_thm thm);
   2.194    in thy |>
   2.195      ConstAlias.map (fn (alias, classes) =>
   2.196 -      ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
   2.197 +      ((c_c', thm) :: alias, insert (op =) class classes))
   2.198    end;
   2.199  
   2.200  fun resubst_alias thy =
   2.201 @@ -306,19 +288,6 @@
   2.202  val triv_classes = snd o ConstAlias.get;
   2.203  
   2.204  
   2.205 -(* reading constants as terms *)
   2.206 -
   2.207 -fun check_bare_const thy t = case try dest_Const t
   2.208 - of SOME c_ty => c_ty
   2.209 -  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   2.210 -
   2.211 -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
   2.212 -
   2.213 -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
   2.214 -
   2.215 -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
   2.216 -
   2.217 -
   2.218  (* constructor sets *)
   2.219  
   2.220  fun constrset_of_consts thy cs =
   2.221 @@ -440,8 +409,6 @@
   2.222  
   2.223  fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr);
   2.224  
   2.225 -val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   2.226 -
   2.227  
   2.228  (*those following are permissive wrt. to overloaded constants!*)
   2.229  
   2.230 @@ -456,14 +423,14 @@
   2.231    o try_thm (gen_assert_eqn thy is_constr_head (K true))
   2.232    o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   2.233  
   2.234 -fun const_typ_eqn_unoverload thy thm =
   2.235 +fun const_typ_eqn thy thm =
   2.236    let
   2.237 -    val (c, ty) = const_typ_eqn thm;
   2.238 +    val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   2.239      val c' = AxClass.unoverload_const thy (c, ty);
   2.240    in (c', ty) end;
   2.241  
   2.242 -fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy;
   2.243 -fun const_eqn thy = fst o const_typ_eqn_unoverload thy;
   2.244 +fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
   2.245 +fun const_eqn thy = fst o const_typ_eqn thy;
   2.246  
   2.247  
   2.248  (* case cerificates *)
   2.249 @@ -787,7 +754,7 @@
   2.250      val dtyps = the_dtyps exec
   2.251        |> Symtab.dest
   2.252        |> map (fn (dtco, (_, (vs, cos)) :: _) =>
   2.253 -          (Syntax.string_of_typ_global thy (Type (dtco, map TFree vs)), cos))
   2.254 +          (string_of_typ thy (Type (dtco, map TFree vs)), cos))
   2.255        |> sort (string_ord o pairself fst)
   2.256    in
   2.257      (Pretty.writeln o Pretty.chunks) [
   2.258 @@ -817,7 +784,7 @@
   2.259              val max' = Thm.maxidx_of thm' + 1;
   2.260            in (thm', max') end;
   2.261          val (thms', maxidx) = fold_map incr_thm thms 0;
   2.262 -        val ty1 :: tys = map (snd o const_typ_eqn) thms';
   2.263 +        val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
   2.264          fun unify ty env = Sign.typ_unify thy (ty1, ty) env
   2.265            handle Type.TUNIFY =>
   2.266              error ("Type unificaton failed, while unifying code equations\n"
   2.267 @@ -963,19 +930,6 @@
   2.268    Symtab.dest ((the_eqns o the_exec) thy)
   2.269    |> maps (Lazy.force o snd o snd o fst o snd);
   2.270  
   2.271 -fun default_typscheme thy c =
   2.272 -  let
   2.273 -    fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const
   2.274 -      o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c;
   2.275 -    fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
   2.276 -  in case AxClass.class_of_param thy c
   2.277 -   of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
   2.278 -    | NONE => if is_constr thy c
   2.279 -        then strip_sorts (the_const_typscheme c)
   2.280 -        else case get_eqns thy c
   2.281 -         of (thm, _) :: _ => (typscheme_eqn thy o Drule.zero_var_indexes) thm
   2.282 -          | [] => strip_sorts (the_const_typscheme c) end;
   2.283 -
   2.284  end; (*struct*)
   2.285  
   2.286  
     3.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 07 17:21:26 2009 +0200
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 07 17:21:27 2009 +0200
     3.3 @@ -102,6 +102,15 @@
     3.4  
     3.5  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
     3.6  
     3.7 +fun eqn_conv conv =
     3.8 +  let
     3.9 +    fun lhs_conv ct = if can Thm.dest_comb ct
    3.10 +      then Conv.combination_conv lhs_conv conv ct
    3.11 +      else Conv.all_conv ct;
    3.12 +  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
    3.13 +
    3.14 +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
    3.15 +
    3.16  fun term_of_conv thy f =
    3.17    Thm.cterm_of thy
    3.18    #> f
    3.19 @@ -117,7 +126,7 @@
    3.20    in
    3.21      eqns
    3.22      |> apply_functrans thy c functrans
    3.23 -    |> (map o apfst) (Code.rewrite_eqn pre)
    3.24 +    |> (map o apfst) (rewrite_eqn pre)
    3.25      |> (map o apfst) (AxClass.unoverload thy)
    3.26      |> map (Code.assert_eqn thy)
    3.27      |> burrow_fst (Code.norm_args thy)
    3.28 @@ -213,9 +222,19 @@
    3.29    (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    3.30      (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
    3.31  
    3.32 +fun default_typscheme_of thy c =
    3.33 +  let
    3.34 +    val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
    3.35 +      o Type.strip_sorts o Sign.the_const_type thy) c;
    3.36 +  in case AxClass.class_of_param thy c
    3.37 +   of SOME class => ([(Name.aT, [class])], ty)
    3.38 +    | NONE => Code.typscheme thy (c, ty)
    3.39 +  end;
    3.40 +
    3.41  fun tyscm_rhss_of thy c eqns =
    3.42    let
    3.43 -    val tyscm = case eqns of [] => Code.default_typscheme thy c
    3.44 +    val tyscm = case eqns
    3.45 +     of [] => default_typscheme_of thy c
    3.46        | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
    3.47      val rhss = consts_of thy eqns;
    3.48    in (tyscm, rhss) end;
    3.49 @@ -381,6 +400,17 @@
    3.50         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
    3.51    end;
    3.52  
    3.53 +fun inst_thm thy tvars' thm =
    3.54 +  let
    3.55 +    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    3.56 +    val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
    3.57 +    fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
    3.58 +     of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
    3.59 +          (tvar, (v, inter_sort (sort, sort'))))
    3.60 +      | NONE => NONE;
    3.61 +    val insts = map_filter mk_inst tvars;
    3.62 +  in Thm.instantiate (insts, []) thm end;
    3.63 +
    3.64  fun add_arity thy vardeps (class, tyco) =
    3.65    AList.default (op =)
    3.66      ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
    3.67 @@ -394,7 +424,7 @@
    3.68      val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
    3.69        Vartab.update ((v, 0), sort)) lhs;
    3.70      val eqns = proto_eqns
    3.71 -      |> (map o apfst) (Code.inst_thm thy inst_tab);
    3.72 +      |> (map o apfst) (inst_thm thy inst_tab);
    3.73      val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
    3.74      val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
    3.75    in (map (pair c) rhss' @ rhss, eqngr') end;
     4.1 --- a/src/Tools/Code/code_target.ML	Tue Jul 07 17:21:26 2009 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Tue Jul 07 17:21:27 2009 +0200
     4.3 @@ -286,7 +286,7 @@
     4.4  fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
     4.5    let
     4.6      val c = prep_const thy raw_c;
     4.7 -    fun check_args (syntax as (n, _)) = if n > Code.no_args thy c
     4.8 +    fun check_args (syntax as (n, _)) = if n > Code.args_number thy c
     4.9        then error ("Too many arguments in syntax for constant " ^ quote c)
    4.10        else syntax;
    4.11    in case raw_syn
     5.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jul 07 17:21:26 2009 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jul 07 17:21:27 2009 +0200
     5.3 @@ -627,8 +627,8 @@
     5.4      fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
     5.5      val tys = arg_types num_args (snd c_ty);
     5.6      val ty = nth tys t_pos;
     5.7 -    fun mk_constr c t = let val n = Code.no_args thy c
     5.8 -      in ((c, arg_types (Code.no_args thy c) (fastype_of t) ---> ty), n) end;
     5.9 +    fun mk_constr c t = let val n = Code.args_number thy c
    5.10 +      in ((c, arg_types n (fastype_of t) ---> ty), n) end;
    5.11      val constrs = if null case_pats then []
    5.12        else map2 mk_constr case_pats (nth_drop t_pos ts);
    5.13      fun casify naming constrs ty ts =
     6.1 --- a/src/Tools/nbe.ML	Tue Jul 07 17:21:26 2009 +0200
     6.2 +++ b/src/Tools/nbe.ML	Tue Jul 07 17:21:27 2009 +0200
     6.3 @@ -393,10 +393,11 @@
     6.4            let
     6.5              val ts' = take_until is_dict ts;
     6.6              val c = const_of_idx idx;
     6.7 -            val (_, T) = Code.default_typscheme thy c;
     6.8 -            val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T;
     6.9 +            val T = map_type_tvar (fn ((v, i), _) =>
    6.10 +              TypeInfer.param typidx (v ^ string_of_int i, []))
    6.11 +                (Sign.the_const_type thy c);
    6.12              val typidx' = typidx + 1;
    6.13 -          in of_apps bounds (Term.Const (c, T'), ts') typidx' end
    6.14 +          in of_apps bounds (Term.Const (c, T), ts') typidx' end
    6.15        | of_univ bounds (BVar (n, ts)) typidx =
    6.16            of_apps bounds (Bound (bounds - n - 1), ts) typidx
    6.17        | of_univ bounds (t as Abs _) typidx =