src/Tools/nbe.ML
changeset 24423 ae9cd0e92423
parent 24381 560e8ecdf633
child 24493 d4380e9b287b
     1.1 --- a/src/Tools/nbe.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val app: Univ -> Univ -> Univ              (*explicit application*)
     1.5  
     1.6    val univs_ref: Univ list ref 
     1.7 -  val lookup_fun: CodeName.const -> Univ
     1.8 +  val lookup_fun: string -> Univ
     1.9  
    1.10    val normalization_conv: cterm -> thm
    1.11  
    1.12 @@ -295,8 +295,8 @@
    1.13        #>> (fn ts' => list_comb (t, rev ts'))
    1.14      and of_univ bounds (Const (name, ts)) typidx =
    1.15            let
    1.16 -            val SOME (const as (c, _)) = CodeName.const_rev thy name;
    1.17 -            val T = Code.default_typ thy const;
    1.18 +            val SOME c = CodeName.const_rev thy name;
    1.19 +            val T = Code.default_typ thy c;
    1.20              val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T;
    1.21              val typidx' = typidx + maxidx_of_typ T' + 1;
    1.22            in of_apps bounds (Term.Const (c, T'), ts) typidx' end