| changeset 39159 | 0dec18004e75 |
| parent 36945 | 9bec62c10714 |
| child 41228 | e1fce873b814 |
--- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:13:10 2010 +0200 @@ -32,9 +32,9 @@ val dest_Trueprop = HOLogic.dest_Trueprop; val mk_Trueprop = HOLogic.mk_Trueprop; -val atomize = thms "induct_atomize"; -val rulify = thms "induct_rulify"; -val rulify_fallback = thms "induct_rulify_fallback"; +val atomize = @{thms induct_atomize}; +val rulify = @{thms induct_rulify}; +val rulify_fallback = @{thms induct_rulify_fallback}; end;