# HG changeset patch
# User wenzelm
# Date 1132406468 -3600
# Node ID 8f3973d3b2f0af897432c0bf6f345693d3b631fc
# Parent  ad4b8567f6ebd5155ade49b985cdaf78d29cccff
Goal.norm_hhf_protected;

diff -r ad4b8567f6eb -r 8f3973d3b2f0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Nov 19 14:21:07 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Nov 19 14:21:08 2005 +0100
@@ -721,7 +721,7 @@
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   in
-    Goal.norm_hhf'
+    Goal.norm_hhf_protected
     #> Seq.EVERY (rev exp_asms)
     #> Seq.map (fn rule =>
       let
@@ -732,7 +732,7 @@
       in
         rule
         |> Drule.forall_intr_list frees
-        |> Goal.norm_hhf'
+        |> Goal.norm_hhf_protected
         |> Drule.tvars_intr_list tfrees |> #2
       end)
   end;