src/FOLP/simp.ML

                 (ccs ~~ (map (map atomic o prems_of) congs));
     in add_norms(congs,ccs,new_asms) end;
 
 fun normed_rews congs =
   let val add_norms = add_norm_tags congs;
-  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
+  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
 
 val trans_norms = map mk_trans normE_thms;