src/HOL/Tools/smallvalue_generators.ML
changeset 41904 2ae19825f7b6
parent 41903 39fd77f0ae59
equal deleted inserted replaced
41903:39fd77f0ae59 41904:2ae19825f7b6
   338   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   338   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   339   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   339   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   340   
   340   
   341 fun post_process_term t =
   341 fun post_process_term t =
   342   let
   342   let
   343     val _ = tracing (Syntax.string_of_term @{context} t)
       
   344     fun map_Abs f t =
   343     fun map_Abs f t =
   345       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   344       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   346     fun process_args t = case strip_comb t of
   345     fun process_args t = case strip_comb t of
   347       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   346       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   348   in
   347   in