# HG changeset patch
# User huffman
# Date 1199375607 -3600
# Node ID cf41372cfee671aa8685e1fe2e7e637306a591b8
# Parent  230c9c87d739fff873776d0a9a6c5e0d2451575b
fix theorem references

diff -r 230c9c87d739 -r cf41372cfee6 src/HOLCF/Tools/adm_tac.ML
--- 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)