equal
deleted
inserted
replaced
502 (** prepare terms and propositions **) |
502 (** prepare terms and propositions **) |
503 |
503 |
504 (* inferred types of parameters *) |
504 (* inferred types of parameters *) |
505 |
505 |
506 fun infer_type ctxt x = |
506 fun infer_type ctxt x = |
507 Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); |
507 (writeln "#### Proof_Context.infer_type"; |
|
508 Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x))); |
508 |
509 |
509 fun inferred_param x ctxt = |
510 fun inferred_param x ctxt = |
510 let val p = (x, infer_type ctxt (x, dummyT)) |
511 let val p = (x, infer_type ctxt (x, dummyT)) |
511 in (p, ctxt |> Variable.declare_term (Free p)) end; |
512 in (p, ctxt |> Variable.declare_term (Free p)) end; |
512 |
513 |