src/Tools/nbe.ML
changeset 47609 b3dab1892cda
parent 47573 6244475356ba
child 48072 ace701efe203
     1.1 --- a/src/Tools/nbe.ML	Thu Apr 19 18:24:40 2012 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Apr 19 19:18:11 2012 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4    in
     1.5      ct
     1.6      |> (Drule.cterm_fun o map_types o map_type_tfree)
     1.7 -        (fn (v, sort) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     1.8 +        (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     1.9      |> conv
    1.10      |> Thm.strip_shyps
    1.11      |> Thm.varifyT_global
    1.12 @@ -240,7 +240,6 @@
    1.13  local
    1.14    val prefix =     "Nbe.";
    1.15    val name_put =   prefix ^ "put_result";
    1.16 -  val name_ref =   prefix ^ "univs_ref";
    1.17    val name_const = prefix ^ "Const";
    1.18    val name_abss =  prefix ^ "abss";
    1.19    val name_apps =  prefix ^ "apps";