equal
deleted
inserted
replaced
501 |
501 |
502 5. test for refl |
502 5. test for refl |
503 *) |
503 *) |
504 fun clean_tac lthy = |
504 fun clean_tac lthy = |
505 let |
505 let |
506 (* FIXME/TODO produce defs with lthy, like prs and ids *) |
506 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy) |
507 val thy = ProofContext.theory_of lthy; |
|
508 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
|
509 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
507 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
510 val prs = prs_rules_get lthy |
508 val prs = prs_rules_get lthy |
511 val ids = id_simps_get lthy |
509 val ids = id_simps_get lthy |
512 |
510 |
513 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
511 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |