1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:34 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:59 2014 +0200
     1.3 @@ -382,14 +382,18 @@
     1.4        Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
     1.5      end
     1.6    
     1.7 +  exception DECODE
     1.8 +    
     1.9    fun decode_code_eq thm =
    1.10 -    let
    1.11 -      val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
    1.12 -      val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
    1.13 -      fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type
    1.14 -    in
    1.15 -      (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
    1.16 -    end
    1.17 +    if nprems_of thm > 0 then raise DECODE 
    1.18 +    else
    1.19 +      let
    1.20 +        val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
    1.21 +        val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
    1.22 +        fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type
    1.23 +      in
    1.24 +        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
    1.25 +      end
    1.26    
    1.27    fun register_encoded_code_eq thm thy =
    1.28      let
    1.29 @@ -397,6 +401,7 @@
    1.30      in
    1.31        register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
    1.32      end
    1.33 +    handle DECODE => thy
    1.34    
    1.35    val register_code_eq_attribute = Thm.declaration_attribute
    1.36      (fn thm => Context.mapping (register_encoded_code_eq thm) I)