# HG changeset patch
# User berghofe
# Date 1038414304 -3600
# Node ID 8ea7388f66d43db2e8963fae2da3c141643d55b7
# Parent  f8badfef5cf2b86e0d12920a3044d12ed2c65496
- tuned beta_eta_convert
- returned theorem is now in beta-eta normal form

diff -r f8badfef5cf2 -r 8ea7388f66d4 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Wed Nov 27 17:23:19 2002 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Wed Nov 27 17:25:04 2002 +0100
@@ -28,11 +28,8 @@
      | Some thm => thm)
   end;
 
-fun beta_eta_convert thm =
-  let
-    val beta_thm = beta_conversion true (cprop_of thm);
-    val (_, rhs) = Drule.dest_equals (cprop_of beta_thm);
-  in Thm.equal_elim (Thm.transitive beta_thm (eta_conversion rhs)) thm end;
+val beta_eta_convert =
+  MetaSimplifier.fconv_rule MetaSimplifier.beta_eta_conversion;
 
 fun thm_of_proof thy prf =
   let
@@ -53,7 +50,7 @@
           let
             val thm = Thm.implies_intr_hyps (lookup name);
             val {prop, ...} = rep_thm thm;
-            val _ = if prop=prop' then () else
+            val _ = if prop aconv prop' then () else
               error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
                 Sign.string_of_term sg prop ^ "\n\n" ^
                 Sign.string_of_term sg prop');
@@ -98,7 +95,6 @@
 
       | thm_of _ _ _ = error "thm_of_proof: partial proof term";
 
-  in thm_of [] [] prf end;
+  in beta_eta_convert (thm_of [] [] prf) end;
 
 end;
-