equal
deleted
inserted
replaced
297 (if is_body ctxt then ctxt else fix_frees t ctxt) |
297 (if is_body ctxt then ctxt else fix_frees t ctxt) |
298 |> declare_term t; |
298 |> declare_term t; |
299 |
299 |
300 fun invent_types Ss ctxt = |
300 fun invent_types Ss ctxt = |
301 let |
301 let |
302 val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss; |
302 val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss; |
303 val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
303 val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
304 in (tfrees, ctxt') end; |
304 in (tfrees, ctxt') end; |
305 |
305 |
306 |
306 |
307 |
307 |