equal
deleted
inserted
replaced
83 |
83 |
84 instantiation "fun" :: (typerep, typerep) term_of |
84 instantiation "fun" :: (typerep, typerep) term_of |
85 begin |
85 begin |
86 |
86 |
87 definition |
87 definition |
88 "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') |
88 "term_of (f \<Colon> 'a \<Rightarrow> 'b) = |
89 [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" |
89 Const (STR ''Pure.dummy_pattern'') |
|
90 (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" |
90 |
91 |
91 instance .. |
92 instance .. |
92 |
93 |
93 end |
94 end |
94 |
95 |