Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Drule.types_sorts;
authorwenzelm
Wed, 11 Jun 2008 18:02:50 +0200
changeset 27155 30e3bdfbbef1
parent 27154 026f3db3f5c6
child 27156 e9f2d5947887
Drule.types_sorts;
src/HOLCF/Tools/adm_tac.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle