src/HOL/Tools/smallvalue_generators.ML
changeset 40845 15b97bd4b5c0
parent 40840 2f97215e79bf
child 40899 ef6fde932f4c
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:03:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:35:40 2010 +0100
     1.3 @@ -18,14 +18,6 @@
     1.4  
     1.5  (** general term functions **)
     1.6  
     1.7 -fun mk_fun_comp (t, u) =
     1.8 -  let
     1.9 -    val (_, B) = dest_funT (fastype_of t)
    1.10 -    val (C, A) = dest_funT (fastype_of u)
    1.11 -  in
    1.12 -    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
    1.13 -  end;
    1.14 -
    1.15  fun mk_measure f =
    1.16    let
    1.17      val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    1.18 @@ -136,7 +128,7 @@
    1.19    let
    1.20      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    1.21      val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
    1.22 -    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
    1.23 +    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
    1.24        Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    1.25      fun mk_termination_measure T =
    1.26        let