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 =