src/Pure/Tools/codegen_func.ML
changeset 22996 5f82c5f8478e
parent 22916 8caf6da610e2
child 23026 db38b8046294
equal deleted inserted replaced
22995:d8b4f2dc2b1d 22996:5f82c5f8478e
   107                ^ Display.string_of_thm thm)
   107                ^ Display.string_of_thm thm)
   108           else ();
   108           else ();
   109     val _ = map (check 0) args;
   109     val _ = map (check 0) args;
   110   in thm end;
   110   in thm end;
   111 
   111 
   112 val mk_func = assert_func o Conv.fconv_rule Drule.beta_eta_conversion o mk_rew;
   112 val mk_func = assert_func o (*Conv.fconv_rule Drule.beta_eta_conversion o *)mk_rew;
   113 
   113 
   114 fun head_func thm =
   114 fun head_func thm =
   115   let
   115   let
   116     val thy = Thm.theory_of_thm thm;
   116     val thy = Thm.theory_of_thm thm;
   117     val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals
   117     val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals