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