equal
deleted
inserted
replaced
1202 (******************************************) |
1202 (******************************************) |
1203 (******************************************) |
1203 (******************************************) |
1204 (* version with explicit qtrm *) |
1204 (* version with explicit qtrm *) |
1205 (******************************************) |
1205 (******************************************) |
1206 (******************************************) |
1206 (******************************************) |
|
1207 |
|
1208 ML {* |
|
1209 fun atomize_goal thy gl = |
|
1210 let |
|
1211 val vars = map Free (Term.add_frees gl []); |
|
1212 fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm; |
|
1213 val gla = fold lambda_all vars gl |
|
1214 val glf = Type.legacy_freeze gla |
|
1215 val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf)) |
|
1216 in |
|
1217 term_of glac |
|
1218 end |
|
1219 *} |
|
1220 |
1207 |
1221 |
1208 ML {* |
1222 ML {* |
1209 (* builds the relation for respects *) |
1223 (* builds the relation for respects *) |
1210 |
1224 |
1211 fun mk_resp_arg lthy (rty, qty) = |
1225 fun mk_resp_arg lthy (rty, qty) = |