# HG changeset patch
# User wenzelm
# Date 1213200170 -7200
# Node ID 30e3bdfbbef1160f65b53f3bdf44c35b17a63d40
# Parent  026f3db3f5c6262328bc2d77e92b615ac4f26f52
Drule.types_sorts;

diff -r 026f3db3f5c6 -r 30e3bdfbbef1 src/HOLCF/Tools/adm_tac.ML
--- a/src/HOLCF/Tools/adm_tac.ML	Wed Jun 11 18:02:25 2008 +0200
+++ b/src/HOLCF/Tools/adm_tac.ML	Wed Jun 11 18:02:50 2008 +0200
@@ -115,7 +115,7 @@
       val j = Thm.maxidx_of state + 1;
       val parTs = map snd (rev params);
       val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
-      val types = valOf o (fst (types_sorts rule));
+      val types = valOf o (fst (Drule.types_sorts rule));
       val tT = types ("t", j);
       val PT = types ("P", j);
       fun mk_abs [] t = t