diff -r ee8e3eaad24c -r 1105b3b5aa77 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 30 12:35:40 2013 +0200
@@ -125,7 +125,7 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
-    val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
+    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);