src/Pure/Isar/proof_context.ML
changeset 55954 a29aefc88c8d
parent 55951 c07d184aebe9
child 55955 e8f1bf005661
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 13:44:01 2014 +0100
     1.3 @@ -71,10 +71,9 @@
     1.4    val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     1.5      xstring * Position.T -> typ * Position.report list
     1.6    val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
     1.7 -  val check_const_proper: Proof.context -> bool ->
     1.8 -    xstring * Position.T -> term * Position.report list
     1.9 -  val read_const_proper: Proof.context -> bool -> string -> term
    1.10 -  val read_const: Proof.context -> bool -> typ -> string -> term
    1.11 +  val check_const: Proof.context -> {proper: bool, strict: bool} ->
    1.12 +    typ -> xstring * Position.T -> term * Position.report list
    1.13 +  val read_const: Proof.context -> {proper: bool, strict: bool} -> typ -> string -> term
    1.14    val read_arity: Proof.context -> xstring * string list * string -> arity
    1.15    val cert_arity: Proof.context -> arity -> arity
    1.16    val allow_dummies: Proof.context -> Proof.context
    1.17 @@ -470,47 +469,40 @@
    1.18  
    1.19  (* constant names *)
    1.20  
    1.21 -fun check_const_proper ctxt strict (c, pos) =
    1.22 +fun check_const ctxt {proper, strict} ty (c, pos) =
    1.23    let
    1.24      fun err msg = error (msg ^ Position.here pos);
    1.25      val consts = consts_of ctxt;
    1.26 -    val (t as Const (d, _), reports) =
    1.27 -      (case Variable.lookup_const ctxt c of
    1.28 -        SOME d =>
    1.29 +    val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
    1.30 +    val (t, reports) =
    1.31 +      (case (fixed, Variable.lookup_const ctxt c) of
    1.32 +        (SOME x, NONE) =>
    1.33            let
    1.34 -            val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
    1.35 +            val _ = Name.reject_internal (c, [pos]);
    1.36 +            val reports =
    1.37 +              if Context_Position.is_reported ctxt pos then
    1.38 +                [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    1.39 +              else [];
    1.40 +          in (Free (x, infer_type ctxt (x, ty)), reports) end
    1.41 +      | (_, SOME d) =>
    1.42 +          let
    1.43 +            val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
    1.44              val reports =
    1.45                if Context_Position.is_reported ctxt pos
    1.46                then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
    1.47            in (Const (d, T), reports) end
    1.48 -      | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
    1.49 +      | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
    1.50      val _ =
    1.51 -      if strict
    1.52 -      then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
    1.53 -      else ();
    1.54 +      (case (strict, t) of
    1.55 +        (true, Const (d, _)) =>
    1.56 +          (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
    1.57 +      | _ => ());
    1.58    in (t, reports) end;
    1.59  
    1.60 -fun read_const_proper ctxt strict text =
    1.61 +fun read_const ctxt flags ty text =
    1.62    let
    1.63      val (t, reports) =
    1.64 -      check_const_proper ctxt strict (Symbol_Pos.source_content (Syntax.read_token text));
    1.65 -    val _ = Position.reports reports;
    1.66 -  in t end;
    1.67 -
    1.68 -fun read_const ctxt strict ty text =
    1.69 -  let
    1.70 -    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    1.71 -    val _ = Name.reject_internal (c, [pos]);
    1.72 -    val (t, reports) =
    1.73 -      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    1.74 -        (SOME x, false) =>
    1.75 -          let
    1.76 -            val reports =
    1.77 -              if Context_Position.is_reported ctxt pos
    1.78 -              then [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    1.79 -              else [];
    1.80 -          in (Free (x, infer_type ctxt (x, ty)), reports) end
    1.81 -      | _ => check_const_proper ctxt strict (c, pos));
    1.82 +      check_const ctxt flags ty (Symbol_Pos.source_content (Syntax.read_token text));
    1.83      val _ = Position.reports reports;
    1.84    in t end;
    1.85