# HG changeset patch
# User wenzelm
# Date 1004487716 -3600
# Node ID a39798b573441c0fe2c8a2bf8572d6991b5acffc
# Parent  da6ee05d9f3d59825c3d746e14e0c8025262ee41
finish_global: Tactic.norm_hhf;

diff -r da6ee05d9f3d -r a39798b57344 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Oct 31 01:21:31 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Oct 31 01:21:56 2001 +0100
@@ -713,7 +713,7 @@
     val full_name = if name = "" then "" else Sign.full_name (sign_of state) name;
     val result =
       prep_result state t raw_thm
-      |> Drule.standard
+      |> Drule.standard |> Tactic.norm_hhf
       |> curry Thm.name_thm full_name;
 
     val atts =