equal
deleted
inserted
replaced
89 (qconst_data, lthy'') |
89 (qconst_data, lthy'') |
90 end |
90 end |
91 |
91 |
92 fun mk_readable_rsp_thm_eq tm lthy = |
92 fun mk_readable_rsp_thm_eq tm lthy = |
93 let |
93 let |
94 val ctm = cterm_of (Proof_Context.theory_of lthy) tm |
94 val ctm = Proof_Context.cterm_of lthy tm |
95 |
95 |
96 fun norm_fun_eq ctm = |
96 fun norm_fun_eq ctm = |
97 let |
97 let |
98 fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy |
98 fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy |
99 fun erase_quants ctm' = |
99 fun erase_quants ctm' = |