equal
deleted
inserted
replaced
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 |