--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Mar 04 19:53:18 2015 +0100
@@ -178,7 +178,8 @@
fun subst_nonatomic_types [] = I
| subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
-fun lhs_head_of thm = Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))));
+fun lhs_head_of thm =
+ Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm))));
fun mk_predT Ts = Ts ---> HOLogic.boolT;
fun mk_pred1T T = mk_predT [T];
@@ -213,7 +214,7 @@
fun cterm_instantiate_pos cts thm =
let
val cert = Thm.cterm_of (Thm.theory_of_thm thm);
- val vars = Term.add_vars (prop_of thm) [];
+ val vars = Term.add_vars (Thm.prop_of thm) [];
val vars' = rev (drop (length vars - length cts) vars);
val ps = map_filter (fn (_, NONE) => NONE
| (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);