# HG changeset patch
# User wenzelm
# Date 1130531276 -7200
# Node ID 99a307bdfe15ddae225584b7878150699b01ed8c
# Parent  09ab79d4e8e17266a50d1beb82dab332e74ac3b5
renamed Goal.norm_hhf_rule to Goal.norm_hhf;

diff -r 09ab79d4e8e1 -r 99a307bdfe15 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Oct 28 22:27:55 2005 +0200
+++ b/src/Pure/goals.ML	Fri Oct 28 22:27:56 2005 +0200
@@ -381,7 +381,7 @@
     val _ = warn_obsolete ();
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
-    val asms = map (Goal.norm_hhf_rule o assume) As;
+    val asms = map (Goal.norm_hhf o Thm.assume) As;
     fun check NONE = error "prove_goal: tactic failed"
       | check (SOME (thm, _)) = (case nprems_of thm of
             0 => thm