# 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", []);