| changeset 32010 | cb1a1c94b4cd |
| parent 31375 | 815426e7dd3b |
| child 33989 | cb136b5f6050 |
--- a/src/HOL/Tools/numeral.ML Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/Tools/numeral.ML Wed Jul 15 23:48:21 2009 +0200 @@ -39,7 +39,7 @@ val oneT = Thm.ctyp_of_term one; val number_of = @{cpat "number_of"}; -val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); +val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); fun instT T V = Thm.instantiate_cterm ([(V, T)], []);