don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
--- a/src/HOL/Tools/Lifting/lifting_term.ML Wed Feb 12 18:32:55 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Feb 13 14:32:04 2014 +0100
@@ -74,6 +74,8 @@
Thm.transfer thy (#quot_thm (get_quot_data ctxt s))
end
+fun has_pcrel_info ctxt s = is_some (#pcr_info (get_quot_data ctxt s))
+
fun get_pcrel_info ctxt s =
case #pcr_info (get_quot_data ctxt s) of
SOME pcr_info => pcr_info
@@ -576,13 +578,13 @@
end
handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
else
- (let
- val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
- in
- (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
- end
- handle QUOT_THM_INTERNAL _ =>
- (Conv.arg1_conv (all_args_conv parametrize_relation_conv)) ctm)
+ if has_pcrel_info ctxt q then
+ let
+ val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
+ in
+ (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
+ end
+ else Conv.arg1_conv (all_args_conv parametrize_relation_conv) ctm
end
end
else Conv.all_conv ctm