Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
be consistent and produce always rep_eq with =
authorkuncar
Mon, 24 Feb 2014 18:12:40 +0100
changeset 55723 f66371633e13
parent 55722 b6ed5f896ce9
child 55724 7572fc374f80
be consistent and produce always rep_eq with =
src/HOL/Tools/Lifting/lifting_def.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 18:12:40 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 18:12:40 2014 +0100
@@ -265,7 +265,7 @@
     val unabs_def = unabs_all_def ctxt unfolded_def
   in  
     if body_type rty = body_type qty then 
-      SOME (simplify_code_eq ctxt unabs_def)
+      SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
     else 
       let
         val thy = Proof_Context.theory_of ctxt
isabelle