| changeset 28262 | aa7ca36d67fd |
| parent 28090 | 29af3c712d2b |
| child 28308 | d4396a28fb29 |
--- a/src/HOL/Tools/numeral.ML Wed Sep 17 21:27:03 2008 +0200 +++ b/src/HOL/Tools/numeral.ML Wed Sep 17 21:27:08 2008 +0200 @@ -40,7 +40,7 @@ val oneT = Thm.ctyp_of_term one; val number_of = @{cpat "number_of"}; -val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); +val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); fun instT T V = Thm.instantiate_cterm ([(V, T)], []);