# HG changeset patch
# User wenzelm
# Date 1459373570 -7200
# Node ID e6443edaebffc8b742b4231fd6c8e3cbd727a964
# Parent  77bbe5af41c362e75db0bd82157283ec70763a90
more explicit support for object-logic constraint;

diff -r 77bbe5af41c3 -r e6443edaebff src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 30 22:35:41 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Mar 30 23:32:50 2016 +0200
@@ -600,7 +600,7 @@
       let
         val ctxt' =
           ctxt |> is_none (Variable.default_type ctxt x) ?
-            Variable.declare_constraints (Free (x, Mixfix.mixfixT mx));
+            Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
         val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
       in ((t, mx), ctxt') end
   | t => ((t, mx), ctxt));
diff -r 77bbe5af41c3 -r e6443edaebff src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 22:35:41 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 23:32:50 2016 +0200
@@ -130,6 +130,9 @@
   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 ->
@@ -1056,10 +1059,33 @@
 
 (** 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 => Mixfix.mixfixT mx)
+  let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx)
   in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
 fun add_syntax vars ctxt =
diff -r 77bbe5af41c3 -r e6443edaebff src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 22:35:41 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 23:32:50 2016 +0200
@@ -27,7 +27,6 @@
   val reset_pos: mixfix -> mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
-  val mixfixT: 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,9 +117,6 @@
   | mixfix_args (Binder _) = 1
   | mixfix_args (Structure _) = 0;
 
-fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
-  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
-
 
 (* syn_ext_types *)