--- a/src/Pure/Isar/generic_target.ML Tue Apr 03 19:33:46 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 19:49:14 2012 +0200
@@ -121,7 +121,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 defs) asms;
+ val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
(*export fixes*)
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);