# HG changeset patch
# User kuncar
# Date 1392298324 -3600
# Node ID 2cf404a469becbc2a0f38c2a32805b489cfb3b1c
# Parent  6ea67a79110828e0e36188addb1ccffefb30029d
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv

diff -r 6ea67a791108 -r 2cf404a469be src/HOL/Tools/Lifting/lifting_term.ML
--- 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