# HG changeset patch
# User wenzelm
# Date 1178750396 -7200
# Node ID 54d231cbc19a25bdf2a3142cda4d698d8a3e49c1
# Parent  7de3b0ac4189ff57427c48f0eeb49f38b5272b1e
moved conversions to structure Conv;
get_axiom_i;

diff -r 7de3b0ac4189 -r 54d231cbc19a src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Thu May 10 00:39:55 2007 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Thu May 10 00:39:56 2007 +0200
@@ -27,7 +27,7 @@
   end;
 
 val beta_eta_convert =
-  Drule.fconv_rule Drule.beta_eta_conversion;
+  Conv.fconv_rule Drule.beta_eta_conversion;
 
 fun thm_of_proof thy prf =
   let
@@ -56,7 +56,7 @@
           in thm_of_atom thm Ts end
 
       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
-          thm_of_atom (get_axiom thy name) Ts
+          thm_of_atom (get_axiom_i thy name) Ts
 
       | thm_of _ Hs (PBound i) = List.nth (Hs, i)