equal
deleted
inserted
replaced
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) = |