--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Mar 04 19:53:18 2015 +0100
@@ -1343,7 +1343,7 @@
NONE => []
| SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) =>
let
- val ms = map (Logic.count_prems o prop_of) ctr_thms;
+ val ms = map (Logic.count_prems o Thm.prop_of) ctr_thms;
val (raw_goal, goal) = (raw_rhs, rhs)
|> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
#> curry Logic.list_all (map dest_Free fun_args));