src/Pure/Isar/generic_target.ML
changeset 47313 6a0ee401b899
parent 47293 052cd5f1a591
child 52153 f5773a46cf05
equal deleted inserted replaced
47312:344712917580 47313:6a0ee401b899
   119     val cert = Thm.cterm_of thy;
   119     val cert = Thm.cterm_of thy;
   120 
   120 
   121     (*export assumes/defines*)
   121     (*export assumes/defines*)
   122     val th = Goal.norm_result raw_th;
   122     val th = Goal.norm_result raw_th;
   123     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
   123     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
   124     val asms' = map (Raw_Simplifier.rewrite_rule defs) asms;
   124     val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
   125 
   125 
   126     (*export fixes*)
   126     (*export fixes*)
   127     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
   127     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
   128     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
   128     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
   129     val (th'' :: vs) =
   129     val (th'' :: vs) =