fix theorem references

--- a/src/HOLCF/Tools/adm_tac.ML	Thu Jan 03 16:31:53 2008 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Thu Jan 03 16:53:27 2008 +0100
@@ -113,7 +113,7 @@
   let val {thy = sign, maxidx, ...} = rep_thm state;
       val j = maxidx+1;
       val parTs = map snd (rev params);
-      val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
+      val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
       val types = valOf o (fst (types_sorts rule));
       val tT = types ("t", j);
       val PT = types ("P", j);
@@ -167,7 +167,7 @@
                 compose_tac (false, rule, 2) i THEN
                 rtac cont_thm i THEN
                 REPEAT (assume_tac i) THEN
-                rtac adm_chfin i
+                rtac @{thm adm_chfin} i
               end 
           | [] => no_tac)
         end)