src/Pure/Isar/proof_context.ML
changeset 62773 e6443edaebff
parent 62768 5f5f11ee4d37
child 62958 b41c1cb5e251
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 22:35:41 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 23:32:50 2016 +0200
     1.3 @@ -130,6 +130,9 @@
     1.4    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     1.5      Proof.context -> (string * thm list) list * Proof.context
     1.6    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
     1.7 +  val set_object_logic_constraint: Proof.context -> Proof.context
     1.8 +  val restore_object_logic_constraint: Proof.context -> Proof.context -> Proof.context
     1.9 +  val default_constraint: Proof.context -> mixfix -> typ
    1.10    val read_var: binding * string option * mixfix -> Proof.context ->
    1.11      (binding * typ option * mixfix) * Proof.context
    1.12    val cert_var: binding * typ option * mixfix -> Proof.context ->
    1.13 @@ -1056,10 +1059,33 @@
    1.14  
    1.15  (** basic logical entities **)
    1.16  
    1.17 +(* default type constraint *)
    1.18 +
    1.19 +val object_logic_constraint =
    1.20 +  Config.bool
    1.21 +    (Config.declare ("Proof_Context.object_logic_constraint", @{here}) (K (Config.Bool false)));
    1.22 +
    1.23 +val set_object_logic_constraint = Config.put object_logic_constraint true;
    1.24 +fun restore_object_logic_constraint ctxt =
    1.25 +  Config.put object_logic_constraint (Config.get ctxt object_logic_constraint);
    1.26 +
    1.27 +fun default_constraint ctxt mx =
    1.28 +  let
    1.29 +    val A =
    1.30 +      (case (Object_Logic.get_base_sort ctxt, Config.get ctxt object_logic_constraint) of
    1.31 +        (SOME S, true) => Type_Infer.anyT S
    1.32 +      | _ => dummyT);
    1.33 +  in
    1.34 +    (case mx of
    1.35 +      Binder _ => (A --> A) --> A
    1.36 +    | _ => replicate (Mixfix.mixfix_args mx) A ---> A)
    1.37 +  end;
    1.38 +
    1.39 +
    1.40  (* variables *)
    1.41  
    1.42  fun declare_var (x, opt_T, mx) ctxt =
    1.43 -  let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
    1.44 +  let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx)
    1.45    in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
    1.46  
    1.47  fun add_syntax vars ctxt =