changeset 47363 | c7fc95e722ff |
parent 47258 | 880e587eee9f |
child 47371 | 4193098c4ec1 |
--- a/src/HOL/Import/import_rule.ML Wed Apr 04 17:51:12 2012 +0200 +++ b/src/HOL/Import/import_rule.ML Wed Apr 04 20:09:56 2012 +0200 @@ -235,7 +235,7 @@ [SOME rept, SOME abst, SOME cP, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", typ_of ctT)))] @{thm typedef_hol2hollight} - val th4 = meta_mp typedef_th (#type_definition (#2 typedef_info)) + val th4 = typedef_th OF [#type_definition (#2 typedef_info)] in (th4, thy') end