--- a/src/Tools/nbe.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/Tools/nbe.ML Mon May 03 20:13:36 2010 +0200
@@ -105,14 +105,14 @@
|> Drule.cterm_rule Thm.varifyT_global
|> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
(((v, 0), sort), TFree (v, sort'))) vs, []))
- |> Drule.cterm_rule Thm.freezeT
+ |> Drule.cterm_rule Thm.legacy_freezeT
|> conv
|> Thm.varifyT_global
|> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
|> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
(((v, 0), []), TVar ((v, 0), sort))) vs, [])
|> strip_of_class
- |> Thm.freezeT
+ |> Thm.legacy_freezeT
end;
fun lift_triv_classes_rew thy rew t =