# 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