# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333562996 -7200
# Node ID c7fc95e722ff55492b986e860cad234ee8558f91
# Parent  87c0eaf04bad02a12c4fdcd84de9448fcbef4606
HOL/Import typed matches against Isabelle typedef result

diff -r 87c0eaf04bad -r c7fc95e722ff src/HOL/Import/import_rule.ML
--- 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