src/Pure/goals.ML

 fun simple_prove_goal_cterm G f =
   let
     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
           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   in