1.1 --- a/src/Tools/nbe.ML	Mon May 03 16:26:47 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Mon May 03 20:13:36 2010 +0200
     1.3 @@ -105,14 +105,14 @@
     1.4      |> Drule.cterm_rule Thm.varifyT_global
     1.5      |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
     1.6          (((v, 0), sort), TFree (v, sort'))) vs, []))
     1.7 -    |> Drule.cterm_rule Thm.freezeT
     1.8 +    |> Drule.cterm_rule Thm.legacy_freezeT
     1.9      |> conv
    1.10      |> Thm.varifyT_global
    1.11      |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
    1.12      |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
    1.13          (((v, 0), []), TVar ((v, 0), sort))) vs, [])
    1.14      |> strip_of_class
    1.15 -    |> Thm.freezeT
    1.16 +    |> Thm.legacy_freezeT
    1.17    end;
    1.18  
    1.19  fun lift_triv_classes_rew thy rew t =