src/HOL/Tools/smallvalue_generators.ML
changeset 40840 2f97215e79bf
parent 40644 0850a2a16dce
child 40845 15b97bd4b5c0
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 11:32:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 13:09:08 2010 +0100
     1.3 @@ -18,9 +18,6 @@
     1.4  
     1.5  (** general term functions **)
     1.6  
     1.7 -fun dest_funT (Type ("fun",[S, T])) = (S, T)
     1.8 -  | dest_funT T = raise TYPE ("dest_funT", [T], [])
     1.9 - 
    1.10  fun mk_fun_comp (t, u) =
    1.11    let
    1.12      val (_, B) = dest_funT (fastype_of t)