# HG changeset patch # User wenzelm # Date 1333475354 -7200 # Node ID 6a0ee401b8991233dbf9a4dd7317e4740e35e527 # Parent 3447129175803dae01202286daa64d58aa7cbeed more robust re-import wrt. non-HHF assumptions; diff -r 344712917580 -r 6a0ee401b899 src/Pure/Isar/generic_target.ML --- 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' []);