# HG changeset patch
# User kuncar
# Date 1353682404 -3600
# Node ID 7017471769523165f5fbcb2c7fbc8a8fcce56cda
# Parent  b27cf06460805429890f84b1e534d086b0fa1bff
simplified code

diff -r b27cf0646080 -r 701747176952 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Nov 23 15:53:19 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Nov 23 15:53:24 2012 +0100
@@ -43,12 +43,9 @@
   in
     if gen_code andalso is_Const abs_background then
       let
-        val (const_name, typ) = dest_Const abs_background
-        val fake_term = Logic.mk_type typ
-        val (fixed_fake_term, lthy') = yield_singleton(Variable.importT_terms) fake_term lthy
-        val fixed_type = Logic.dest_type fixed_fake_term
+        val (fixed_abs_background, lthy') = yield_singleton(Variable.importT_terms) abs_background lthy
       in  
-         Local_Theory.background_theory(Code.add_datatype [(const_name, fixed_type)]) lthy'
+         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs_background]) lthy'
       end
     else
       lthy