equal
deleted
inserted
replaced
37 |
37 |
38 val one = @{cpat "1"}; |
38 val one = @{cpat "1"}; |
39 val oneT = Thm.ctyp_of_term one; |
39 val oneT = Thm.ctyp_of_term one; |
40 |
40 |
41 val number_of = @{cpat "number_of"}; |
41 val number_of = @{cpat "number_of"}; |
42 val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); |
42 val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); |
43 |
43 |
44 fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
44 fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
45 |
45 |
46 in |
46 in |
47 |
47 |