src/HOL/Import/import_data.ML

 fun add_const_def s th name_opt thy =
   let
     val th = Thm.legacy_freezeT th
     val name = case name_opt of
          NONE => (fst o dest_Const o fst o HOLogic.dest_eq o
-           HOLogic.dest_Trueprop o prop_of) th
+           HOLogic.dest_Trueprop o Thm.prop_of) th
        | SOME n => n
     val thy' = add_const_map s name thy
   in
     Data.map (fn {const_map, ty_map, const_def, ty_def} =>
       {const_map = const_map, ty_map = ty_map,

   end
 
 fun add_typ_def tyname absname repname th thy =
   let
     val th = Thm.legacy_freezeT th
-    val (l, _) = dest_comb (HOLogic.dest_Trueprop (prop_of th))
+    val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
     val (l, abst) = dest_comb l
     val (_, rept) = dest_comb l
     val (absn, _) = dest_Const abst
     val (repn, _) = dest_Const rept
     val nty = domain_type (fastype_of rept)