--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Mar 04 19:53:18 2015 +0100
@@ -53,7 +53,7 @@
fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
- val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+ val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];