diff -r ee3c4ec1d652 -r 3f9341831812 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/src/FOLP/simp.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -221,8 +221,9 @@
     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(Thm.freezeT thm))
+  let val add_norms = add_norm_tags congs in
+    fn thm => Variable.tradeT (Variable.thm_context thm)
+      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];