changeset 18522 | 9bdfb6eaf8ab |
parent 18374 | 598e7fd7438b |
child 18529 | 540da2415751 |
--- a/src/HOL/cladata.ML Fri Dec 30 16:56:54 2005 +0100 +++ b/src/HOL/cladata.ML Fri Dec 30 16:56:56 2005 +0100 @@ -38,7 +38,7 @@ (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***) -structure Make_Elim = Make_Elim_Fun (val classical = classical); +structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl"); (*we don't redeclare the original make_elim (Tactic.make_elim) for compatibliity with strange things done in many existing proofs *)