1.1 --- a/src/HOL/Datatype.thy	Mon Dec 06 09:19:10 2010 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Dec 06 09:25:05 2010 +0100
     1.3 @@ -13,6 +13,12 @@
     1.4    ("Tools/Datatype/datatype_realizer.ML")
     1.5  begin
     1.6  
     1.7 +subsection {* Prelude: lifting over function space *}
     1.8 +
     1.9 +type_lifting map_fun
    1.10 +  by (simp_all add: fun_eq_iff)
    1.11 +
    1.12 +
    1.13  subsection {* The datatype universe *}
    1.14  
    1.15  typedef (Node)

     2.1 --- a/src/HOL/Fun.thy	Mon Dec 06 09:19:10 2010 +0100
     2.2 +++ b/src/HOL/Fun.thy	Mon Dec 06 09:25:05 2010 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  
     2.5  theory Fun
     2.6  imports Complete_Lattice
     2.7 +uses ("Tools/type_lifting.ML")
     2.8  begin
     2.9  
    2.10  text{*As a simplification rule, it replaces all function equalities by
    2.11 @@ -126,9 +127,6 @@
    2.12    "map_fun f g h x = g (h (f x))"
    2.13    by (simp add: map_fun_def)
    2.14  
    2.15 -type_lifting map_fun
    2.16 -  by (simp_all add: fun_eq_iff)
    2.17 -
    2.18  
    2.19  subsection {* Injectivity and Bijectivity *}
    2.20  
    2.21 @@ -774,7 +772,9 @@
    2.22    thus False by best
    2.23  qed
    2.24  
    2.25 -subsection {* Proof tool setup *} 
    2.26 +subsection {* Setup *} 
    2.27 +
    2.28 +subsubsection {* Proof tools *}
    2.29  
    2.30  text {* simplifies terms of the form
    2.31    f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
    2.32 @@ -809,7 +809,7 @@
    2.33  *}
    2.34  
    2.35  
    2.36 -subsection {* Code generator setup *}
    2.37 +subsubsection {* Code generator *}
    2.38  
    2.39  types_code
    2.40    "fun"  ("(_ ->/ _)")
    2.41 @@ -840,4 +840,9 @@
    2.42  code_const "id"
    2.43    (Haskell "id")
    2.44  
    2.45 +
    2.46 +subsubsection {* Functorial structure of types *}
    2.47 +
    2.48 +use "Tools/type_lifting.ML"
    2.49 +
    2.50  end

     3.1 --- a/src/HOL/HOL.thy	Mon Dec 06 09:19:10 2010 +0100
     3.2 +++ b/src/HOL/HOL.thy	Mon Dec 06 09:25:05 2010 +0100
     3.3 @@ -32,7 +32,6 @@
     3.4    "Tools/async_manager.ML"
     3.5    "Tools/try.ML"
     3.6    ("Tools/cnf_funcs.ML")
     3.7 -  ("Tools/type_lifting.ML")
     3.8    "~~/src/Tools/subtyping.ML"
     3.9  begin
    3.10  
    3.11 @@ -714,7 +713,6 @@
    3.12    and [Pure.elim?] = iffD1 iffD2 impE
    3.13  
    3.14  use "Tools/hologic.ML"
    3.15 -use "Tools/type_lifting.ML"
    3.16  
    3.17  
    3.18  subsubsection {* Atomizing meta-level connectives *}

     4.1 --- a/src/HOL/IsaMakefile	Mon Dec 06 09:19:10 2010 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Mon Dec 06 09:25:05 2010 +0100
     4.3 @@ -147,7 +147,6 @@
     4.4    $(SRC)/Tools/solve_direct.ML \
     4.5    $(SRC)/Tools/value.ML \
     4.6    HOL.thy \
     4.7 -  Tools/type_lifting.ML \
     4.8    Tools/hologic.ML \
     4.9    Tools/recfun_codegen.ML \
    4.10    Tools/simpdata.ML
    4.11 @@ -243,6 +242,7 @@
    4.12    Tools/split_rule.ML \
    4.13    Tools/try.ML \
    4.14    Tools/typedef.ML \
    4.15 +  Tools/type_lifting.ML \
    4.16    Transitive_Closure.thy \
    4.17    Typedef.thy \
    4.18    Wellfounded.thy