TFL/rules.ML

--- a/TFL/rules.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/TFL/rules.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -266,7 +266,7 @@
          | DL th (th1::rst) =
             let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
              in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
-   in DL (freezeT disjth) (organize eq tml thl)
+   in DL (Thm.freezeT disjth) (organize eq tml thl)
    end;