equal
deleted
inserted
replaced
190 fun get_calculation_ thy (op_, eval_fn) ct = |
190 fun get_calculation_ thy (op_, eval_fn) ct = |
191 case get_pair thy op_ eval_fn ct of |
191 case get_pair thy op_ eval_fn ct of |
192 NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_); |
192 NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_); |
193 tracing ("@@@ get_calculation: ct= "); atomty ct; *) |
193 tracing ("@@@ get_calculation: ct= "); atomty ct; *) |
194 NONE) |
194 NONE) |
195 | SOME (thmid, t) => SOME (thmid, (make_thm o (cterm_of thy)) t); |
195 | SOME (thmid, t) => SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t); |
196 (* |
196 (* |
197 > val ct = (the o (parse thy)) "#9 is_const"; |
197 > val ct = (the o (parse thy)) "#9 is_const"; |
198 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; |
198 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; |
199 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") |
199 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") |
200 |
200 |
305 *) |
305 *) |
306 fun get_calculation1_ thy ((op_, eval_fn):cal) ct = |
306 fun get_calculation1_ thy ((op_, eval_fn):cal) ct = |
307 case eval_fn op_ ct thy of |
307 case eval_fn op_ ct thy of |
308 NONE => NONE |
308 NONE => NONE |
309 | SOME (thmid,t) => |
309 | SOME (thmid,t) => |
310 SOME (thmid, (make_thm o (cterm_of thy)) t); |
310 SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t); |
311 |
311 |
312 |
312 |
313 |
313 |
314 |
314 |
315 |
315 |