equal
deleted
inserted
replaced
1116 ML {* |
1116 ML {* |
1117 fun atomize_goal thy gl = |
1117 fun atomize_goal thy gl = |
1118 let |
1118 let |
1119 val vars = map Free (Term.add_frees gl []); |
1119 val vars = map Free (Term.add_frees gl []); |
1120 fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm; |
1120 fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm; |
1121 val gla = fold lambda_all vars gl |
1121 val gla = fold lambda_all vars (@{term "Trueprop"} $ gl) |
1122 val glf = Type.legacy_freeze gla |
1122 val glf = Type.legacy_freeze gla |
1123 val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf)) |
1123 val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf)) |
1124 in |
1124 in |
1125 term_of glac |
1125 term_of glac |
1126 end |
1126 end |