1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:53:08 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:55:22 2010 +0200
     1.3 @@ -55,13 +55,13 @@
     1.4    val cert_typ_abbrev: Proof.context -> typ -> typ
     1.5    val get_skolem: Proof.context -> string -> string
     1.6    val revert_skolem: Proof.context -> string -> string
     1.7 -  val infer_type: Proof.context -> string -> typ
     1.8 +  val infer_type: Proof.context -> string * typ -> typ
     1.9    val inferred_param: string -> Proof.context -> typ * Proof.context
    1.10    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    1.11    val read_type_name: Proof.context -> bool -> string -> typ
    1.12    val read_type_name_proper: Proof.context -> bool -> string -> typ
    1.13    val read_const_proper: Proof.context -> bool -> string -> term
    1.14 -  val read_const: Proof.context -> bool -> string -> term
    1.15 +  val read_const: Proof.context -> bool -> typ -> string -> term
    1.16    val allow_dummies: Proof.context -> Proof.context
    1.17    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
    1.18    val check_tfree: Proof.context -> string * sort -> string * sort
    1.19 @@ -438,11 +438,10 @@
    1.20  (* inferred types of parameters *)
    1.21  
    1.22  fun infer_type ctxt x =
    1.23 -  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt))
    1.24 -    (Free (x, dummyT)));
    1.25 +  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
    1.26  
    1.27  fun inferred_param x ctxt =
    1.28 -  let val T = infer_type ctxt x
    1.29 +  let val T = infer_type ctxt (x, dummyT)
    1.30    in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
    1.31  
    1.32  fun inferred_fixes ctxt =
    1.33 @@ -505,13 +504,13 @@
    1.34  
    1.35  fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
    1.36  
    1.37 -fun read_const ctxt strict text =
    1.38 +fun read_const ctxt strict ty text =
    1.39    let val (c, pos) = token_content text in
    1.40      (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    1.41        (SOME x, false) =>
    1.42          (Position.report (Markup.name x
    1.43              (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
    1.44 -          Free (x, infer_type ctxt x))
    1.45 +          Free (x, infer_type ctxt (x, ty)))
    1.46      | _ => prep_const_proper ctxt strict (c, pos))
    1.47    end;
    1.48