src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/Isar/code.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -686,7 +686,7 @@
 
 fun get_head thy cert_thm =
   let
-    val [head] = (#hyps o Thm.crep_thm) cert_thm;
+    val [head] = Thm.chyps_of cert_thm;
     val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
   in (typscheme thy (c, ty), head) end;