--- a/src/HOL/Import/proof_kernel.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon May 03 16:26:47 2010 +0200
@@ -2065,7 +2065,7 @@
let
val (HOLThm args) = norm_hthm (theory_of_thm th) hth
in
- apsnd strip_shyps args
+ apsnd Thm.strip_shyps args
end
fun to_isa_term tm = tm