src/HOL/Import/import_rule.ML
changeset 47363 c7fc95e722ff
parent 47258 880e587eee9f
child 47371 4193098c4ec1
equal deleted inserted replaced
47361:87c0eaf04bad 47363:c7fc95e722ff
   233        Drule.instantiate'
   233        Drule.instantiate'
   234           [SOME nty, SOME oty]
   234           [SOME nty, SOME oty]
   235           [SOME rept, SOME abst, SOME cP, SOME (cterm_of thy' (Free ("a", aty))),
   235           [SOME rept, SOME abst, SOME cP, SOME (cterm_of thy' (Free ("a", aty))),
   236              SOME (cterm_of thy' (Free ("r", typ_of ctT)))]
   236              SOME (cterm_of thy' (Free ("r", typ_of ctT)))]
   237           @{thm typedef_hol2hollight}
   237           @{thm typedef_hol2hollight}
   238     val th4 = meta_mp typedef_th (#type_definition (#2 typedef_info))
   238     val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
   239   in
   239   in
   240     (th4, thy')
   240     (th4, thy')
   241   end
   241   end
   242 
   242 
   243 fun mtydef name thy =
   243 fun mtydef name thy =