equal
deleted
inserted
replaced
365 Variable.add_fixes (map fst lsrs) |> snd |> |
365 Variable.add_fixes (map fst lsrs) |> snd |> |
366 Proof.theorem_i NONE |
366 Proof.theorem_i NONE |
367 (fn thss => fn goal_ctxt => |
367 (fn thss => fn goal_ctxt => |
368 let |
368 let |
369 val simps = ProofContext.export goal_ctxt lthy' (flat thss); |
369 val simps = ProofContext.export goal_ctxt lthy' (flat thss); |
370 val (simps', lthy'') = fold_map (LocalTheory.note Thm.generated_theoremK) |
370 val (simps', lthy'') = fold_map (LocalTheory.note Thm.generatedK) |
371 (names_atts' ~~ map single simps) lthy' |
371 (names_atts' ~~ map single simps) lthy' |
372 in |
372 in |
373 lthy'' |
373 lthy'' |
374 |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"), |
374 |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"), |
375 map (Attrib.internal o K) |
375 map (Attrib.internal o K) |
376 [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), |
376 [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), |
377 maps snd simps') |
377 maps snd simps') |
378 |> snd |
378 |> snd |
379 end) |
379 end) |