# HG changeset patch
# User blanchet
# Date 1390257822 -3600
# Node ID 9475b16e520b46d543cadafaffa5e75a05c4471c
# Parent  181751ad852f41b97be18c08e9f1e52b3562c885
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'

diff -r 181751ad852f -r 9475b16e520b src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Mon Jan 20 23:34:26 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Mon Jan 20 23:43:42 2014 +0100
@@ -5,7 +5,7 @@
 header {* Setup for Lifting/Transfer for the option type *}
 
 theory Lifting_Option
-imports Lifting Option
+imports Lifting Partial_Function
 begin
 
 subsection {* Relator and predicator properties *}
@@ -115,4 +115,3 @@
 end
 
 end
-