--- a/src/Pure/Proof/extraction.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 28 11:53:09 2015 +0200
@@ -364,7 +364,7 @@
let
val S = Sign.defaultS thy;
val ((atyp_map, constraints, _), prop') =
- Logic.unconstrainT (#shyps (Thm.rep_thm thm)) (Thm.prop_of thm);
+ Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
SOME (TVar (("'" ^ v, i), [])) else NONE)