# HG changeset patch
# User kuncar
# Date 1406226119 -7200
# Node ID 179b9c43fe84b4cd761dca25204c27561706c23f
# Parent  b590fcd03a4aa0a9c46818112ccd203b878bb1a6
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations

diff -r b590fcd03a4a -r 179b9c43fe84 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:34 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:59 2014 +0200
@@ -382,14 +382,18 @@
       Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
     end
   
+  exception DECODE
+    
   fun decode_code_eq thm =
-    let
-      val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
-      val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
-      fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type
-    in
-      (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
-    end
+    if nprems_of thm > 0 then raise DECODE 
+    else
+      let
+        val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
+        val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
+        fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type
+      in
+        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
+      end
   
   fun register_encoded_code_eq thm thy =
     let
@@ -397,6 +401,7 @@
     in
       register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
     end
+    handle DECODE => thy
   
   val register_code_eq_attribute = Thm.declaration_attribute
     (fn thm => Context.mapping (register_encoded_code_eq thm) I)