# HG changeset patch # User wenzelm # Date 1460465453 -7200 # Node ID 19c2a58623ed2316d0626dfefe96708763a72acb # Parent b41c1cb5e251403102eb715da0e0ca44ce482cf3 back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff); diff -r b41c1cb5e251 -r 19c2a58623ed src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Apr 12 14:38:57 2016 +0200 +++ b/src/Pure/Isar/proof.ML Tue Apr 12 14:50:53 2016 +0200 @@ -600,7 +600,7 @@ let val ctxt' = ctxt |> is_none (Variable.default_type ctxt x) ? - Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx)); + Variable.declare_constraints (Free (x, Mixfix.default_constraint mx)); val t = Free (#1 (Proof_Context.inferred_param x ctxt')); in ((t, mx), ctxt') end | t => ((t, mx), ctxt)); diff -r b41c1cb5e251 -r 19c2a58623ed src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 12 14:38:57 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 12 14:50:53 2016 +0200 @@ -130,9 +130,6 @@ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context - val set_object_logic_constraint: Proof.context -> Proof.context - val restore_object_logic_constraint: Proof.context -> Proof.context -> Proof.context - val default_constraint: Proof.context -> mixfix -> typ val read_var: binding * string option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val cert_var: binding * typ option * mixfix -> Proof.context -> @@ -1059,33 +1056,10 @@ (** basic logical entities **) -(* default type constraint *) - -val object_logic_constraint = - Config.bool - (Config.declare ("Proof_Context.object_logic_constraint", @{here}) (K (Config.Bool false))); - -val set_object_logic_constraint = Config.put object_logic_constraint true; -fun restore_object_logic_constraint ctxt = - Config.put object_logic_constraint (Config.get ctxt object_logic_constraint); - -fun default_constraint ctxt mx = - let - val A = - (case (Object_Logic.get_base_sort ctxt, Config.get ctxt object_logic_constraint) of - (SOME S, true) => Type_Infer.anyT S - | _ => dummyT); - in - (case mx of - Binder _ => (A --> A) --> A - | _ => replicate (Mixfix.mixfix_args mx) A ---> A) - end; - - (* variables *) fun declare_var (x, opt_T, mx) ctxt = - let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx) + let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx) in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end; fun add_syntax vars ctxt = diff -r b41c1cb5e251 -r 19c2a58623ed src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Apr 12 14:38:57 2016 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Apr 12 14:50:53 2016 +0200 @@ -27,6 +27,7 @@ val reset_pos: mixfix -> mixfix val pretty_mixfix: mixfix -> Pretty.T val mixfix_args: mixfix -> int + val default_constraint: mixfix -> typ val make_type: int -> typ val binder_name: string -> string val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext @@ -118,6 +119,12 @@ | mixfix_args (Structure _) = 0; +(* default type constraint *) + +fun default_constraint (Binder _) = (dummyT --> dummyT) --> dummyT + | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT; + + (* syn_ext_types *) val typeT = Type ("type", []);