src/HOL/Tools/record_package.ML

                  list_all ((fst r,rT)::vars,
                            app_bounds (n - 1) ((Free P)$Bound n))); 
     val prove_standard = quick_and_dirty_prove true thy;
     val thm = prove_standard [] prop (fn prems =>
 	 EVERY [rtac equal_intr_rule 1, 
-                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
-                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
+                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
+                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   in thm end
   | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
 
 in
 (* During proof of theorems produced by record_simproc you can end up in

                   simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1]));
     val surjective = timeit_msg "record extension surjective proof:" surjective_prf;
 
     fun split_meta_prf () =
         prove_standard [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
                 etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
                 REPEAT (etac meta_allE 1), atac 1]);
     val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
 

         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
     val cases = timeit_msg "record cases proof:" cases_prf;
 
     fun split_meta_prf () =
         prove false [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
                 etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
                 REPEAT (etac meta_allE 1), atac 1]);
     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
     val split_meta_standard = standard split_meta;