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.
moved conversions to structure Conv;
authorwenzelm
Thu, 10 May 2007 00:39:56 +0200
changeset 22910 54d231cbc19a
parent 22909 7de3b0ac4189
child 22911 2f5e8d70a179
moved conversions to structure Conv; get_axiom_i;
src/Pure/Proof/proofchecker.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle