equal
deleted
inserted
replaced
418 (* augment context by implicit term declarations *) |
418 (* augment context by implicit term declarations *) |
419 |
419 |
420 fun augment t ctxt = ctxt |
420 fun augment t ctxt = ctxt |
421 |> not (Variable.is_body ctxt) ? |
421 |> not (Variable.is_body ctxt) ? |
422 Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t [])) |
422 Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t [])) |
423 |> Variable.declare_term t; |
423 |> Variable.declare_term t |
|
424 |> Soft_Type_System.augment t; |
424 |
425 |
425 |
426 |
426 |
427 |
427 (** pretty printing **) |
428 (** pretty printing **) |
428 |
429 |