# HG changeset patch
# User wenzelm
# Date 1460466066 -7200
# Node ID 8b85a554c5c4aee713947c8e9b52398761d1c443
# Parent  f59ef58f420b71d73dd431d2b21c20e9c547e902# Parent  cfbb6a5b427c1fed6d2188d32d5b371f6c941cc5
merged

diff -r f59ef58f420b -r 8b85a554c5c4 NEWS
--- a/NEWS	Tue Apr 12 11:18:29 2016 +0200
+++ b/NEWS	Tue Apr 12 15:01:06 2016 +0200
@@ -9,6 +9,13 @@
 
 *** General ***
 
+* Type-inference improves sorts of newly introduced type variables for
+the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
+Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
+produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
+INCOMPATIBILITY, need to provide explicit type constraints for Pure
+types where this is really intended.
+
 * Mixfix annotations support general block properties, with syntax
 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -69,6 +69,7 @@
 subsection \<open>Tools setup and evaluation\<close>
 
 lemma eq_eq_TrueD:
+  fixes x y :: "'a::{}"
   assumes "(x \<equiv> y) \<equiv> Trueprop True"
   shows "x \<equiv> y"
   using assms by simp
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -747,7 +747,7 @@
 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   by (rule classical) iprover
 
-lemma thin_refl: "\<And>X. \<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
+lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
 
 ML \<open>
 structure Hypsubst = Hypsubst
@@ -1506,7 +1506,7 @@
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
-lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
+lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the list type\<close>
 
 theory Quotient_List
-imports Main Quotient_Set Quotient_Product Quotient_Option
+imports Quotient_Set Quotient_Product Quotient_Option
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the option type\<close>
 
 theory Quotient_Option
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the product type\<close>
 
 theory Quotient_Product
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the set type\<close>
 
 theory Quotient_Set
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the sum type\<close>
 
 theory Quotient_Sum
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -1052,7 +1052,7 @@
         val deadfixed_T =
           build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
           |> singleton (Type_Infer_Context.infer_types lthy)
-          |> singleton (Type_Infer.fixate lthy)
+          |> singleton (Type_Infer.fixate lthy false)
           |> type_of
           |> dest_funT
           |-> generalize_types 1
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -80,11 +80,7 @@
 
 fun prepare_function do_print prep fixspec eqns config lthy =
   let
-    val ((fixes0, spec0), ctxt') =
-      lthy
-      |> Proof_Context.set_object_logic_constraint
-      |> prep fixspec eqns
-      ||> Proof_Context.restore_object_logic_constraint lthy;
+    val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy;
     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -120,7 +120,7 @@
       th RS @{thm eq_reflection}
   | _ => th)
 
-val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+val meta_fun_cong = @{lemma "\<And>f :: 'a::{} \<Rightarrow> 'b::{}.f == g ==> f x == g x" by simp}
 
 fun full_fun_cong_expand th =
   let
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -134,18 +134,14 @@
     val (opt_var, ctxt) =
       (case raw_var of
         NONE => (NONE, lthy)
-      | SOME var =>
-          Proof_Context.set_object_logic_constraint lthy
-          |> prep_var var
-          ||> Proof_Context.restore_object_logic_constraint lthy
-          |>> SOME)
-    val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT)
+      | SOME var => prep_var var lthy |>> SOME)
+    val lhs_constraints = (case opt_var of SOME (_, SOME T, _) => [T] | _ => [])
 
-    fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
-    val lhs = prep_term lhs_constraint raw_lhs
-    val rhs = prep_term dummyT raw_rhs
+    fun prep_term Ts = parse_term ctxt #> fold Type.constraint Ts #> Syntax.check_term ctxt;
+    val lhs = prep_term lhs_constraints raw_lhs
+    val rhs = prep_term [] raw_rhs
 
-    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined"
     val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
 
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -518,8 +518,7 @@
         end
       | go _ ctxt = dummy ctxt
   in
-    go t ctxt |> fst |> Syntax.check_term ctxt |>
-      map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
+    go t ctxt |> fst |> Syntax.check_term ctxt
   end
 
 (** Monotonicity analysis **)
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -165,9 +165,9 @@
       | NONE => NONE)
   | subst_termify t = subst_termify_app (strip_comb t) 
 
-fun check_termify _ ts = the_default ts (map_default subst_termify ts);
+fun check_termify ts = the_default ts (map_default subst_termify ts);
 
-val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
 
 
 (** evaluation **)
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/record.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -1063,7 +1063,7 @@
 *)
 val simproc =
   Simplifier.make_simproc @{context} "record"
-   {lhss = [@{term "x"}],
+   {lhss = [@{term "x::'a::{}"}],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1147,7 +1147,7 @@
   both a more update and an update to a field within it.*)
 val upd_simproc =
   Simplifier.make_simproc @{context} "record_upd"
-   {lhss = [@{term "x"}],
+   {lhss = [@{term "x::'a::{}"}],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1292,7 +1292,7 @@
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
   Simplifier.make_simproc @{context} "record_split"
-   {lhss = [@{term x}],
+   {lhss = [@{term "x::'a::{}"}],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -534,7 +534,7 @@
 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
   by (blast elim: tranclE dest: trancl_into_rtrancl)
 
-lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
+lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r^+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y"
   by (blast dest: r_into_trancl)
 
 lemma trancl_subset_Sigma_aux:
diff -r f59ef58f420b -r 8b85a554c5c4 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 12 15:01:06 2016 +0200
@@ -993,7 +993,7 @@
 lemma bin_rsplit_size_sign' [rule_format] : 
   "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
     (ALL v: set sw. bintrunc n v = v)"
-  apply (induct sw arbitrary: nw w v)
+  apply (induct sw arbitrary: nw w)
    apply clarsimp
   apply clarsimp
   apply (drule bthrs)
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -107,7 +107,6 @@
 
 fun prep_class_elems prep_decl thy sups raw_elems =
   let
-
     (* user space type system: only permits 'a type variable, improves towards 'a *)
     val algebra = Sign.classes_of thy;
     val inter_sort = curry (Sorts.inter_sort algebra);
@@ -118,7 +117,7 @@
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd)
         (Class.these_operations thy sups);
-    fun singleton_fixateT Ts =
+    val singleton_fixate = burrow_types (fn Ts =>
       let
         val tfrees = fold Term.add_tfreesT Ts [];
         val inferred_sort =
@@ -140,9 +139,8 @@
       in
         (map o map_atyps)
           (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
-      end;
-    fun singleton_fixate _ ts = burrow_types singleton_fixateT ts;
-    fun unify_params ctxt ts =
+      end);
+    fun unify_params ts =
       let
         val param_Ts = (fold o fold_aterms)
           (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts [];
@@ -162,10 +160,10 @@
     val init_class_body =
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" singleton_fixate);
+      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems, _), _) =
       Proof_Context.init_global thy
-      |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" unify_params)
+      |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -175,7 +175,7 @@
     val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
     val arg = type_parms @ map2 Type.constraint parm_types' insts';
-    val res = Syntax.check_terms ctxt arg;
+    val res = Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) arg;
     val ctxt' = ctxt |> fold Variable.auto_fixes res;
 
     (* instantiation *)
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 12 15:01:06 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 f59ef58f420b -r 8b85a554c5c4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 12 15:01:06 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 ->
@@ -666,7 +663,7 @@
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    Type_Infer.fixate ctxt #>
+    Type_Infer.fixate ctxt pattern #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -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 f59ef58f420b -r 8b85a554c5c4 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -167,8 +167,9 @@
 fun read_term ctxt T s =
   let
     val ctxt' = ctxt
-      |> Config.put Type_Infer_Context.const_sorts false
-      |> Proof_Context.set_defsort [];
+      |> Proof_Context.set_defsort []
+      |> Config.put Type_Infer.object_logic false
+      |> Config.put Type_Infer_Context.const_sorts false;
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
 
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -215,7 +215,10 @@
       |> Proof_Context.init_global
       |> Proof_Context.allow_dummies
       |> Proof_Context.set_mode Proof_Context.mode_schematic
-      |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
+      |> topsort ?
+        (Proof_Context.set_defsort [] #>
+         Config.put Type_Infer.object_logic false #>
+         Config.put Type_Infer_Context.const_sorts false);
   in
     fn ty => fn s =>
       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Apr 12 15:01:06 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", []);
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -970,18 +970,7 @@
 end;
 
 
-(* standard phases *)
-
-val _ = Context.>>
- (typ_check 0 "standard" Proof_Context.standard_typ_check #>
-  term_check 0 "standard"
-    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
-  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
-  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
-
-
-
-(** install operations **)
+(* install operations *)
 
 val _ =
   Theory.setup
@@ -1000,3 +989,13 @@
       uncheck_terms = uncheck_terms});
 
 end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
+  Syntax_Phases.term_check 0 "standard"
+    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+  Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+  Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Tue Apr 12 15:01:06 2016 +0200
@@ -50,34 +50,27 @@
 
   /* internal tools */
 
-  private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
+  private val internal_tools: List[Isabelle_Tool] =
+    List(
+      Build.isabelle_tool,
+      Build_Doc.isabelle_tool,
+      Check_Sources.isabelle_tool,
+      Doc.isabelle_tool,
+      ML_Process.isabelle_tool,
+      Options.isabelle_tool,
+      Update_Cartouches.isabelle_tool,
+      Update_Header.isabelle_tool,
+      Update_Then.isabelle_tool,
+      Update_Theorems.isabelle_tool)
 
   private def list_internal(): List[(String, String)] =
-    synchronized {
-      for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
-    }
+    for (tool <- internal_tools.toList) yield (tool.name, tool.description)
 
   private def find_internal(name: String): Option[List[String] => Unit] =
-    synchronized { internal_tools.get(name).map(_._2) }
-
-  private def register(isabelle_tool: Isabelle_Tool): Unit =
-    synchronized {
-      internal_tools +=
-        (isabelle_tool.name ->
-          (isabelle_tool.description,
-            args => Command_Line.tool0 { isabelle_tool.body(args) }))
-    }
-
-  register(Build.isabelle_tool)
-  register(Build_Doc.isabelle_tool)
-  register(Check_Sources.isabelle_tool)
-  register(Doc.isabelle_tool)
-  register(ML_Process.isabelle_tool)
-  register(Options.isabelle_tool)
-  register(Update_Cartouches.isabelle_tool)
-  register(Update_Header.isabelle_tool)
-  register(Update_Then.isabelle_tool)
-  register(Update_Theorems.isabelle_tool)
+    internal_tools.collectFirst({
+      case tool if tool.name == name =>
+        args => Command_Line.tool0 { tool.body(args) }
+      })
 
 
   /* command line entry point */
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/type_infer.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -16,7 +16,8 @@
   val paramify_vars: typ -> typ
   val deref: typ Vartab.table -> typ -> typ
   val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
-  val fixate: Proof.context -> term list -> term list
+  val object_logic: bool Config.T
+  val fixate: Proof.context -> bool -> term list -> term list
 end;
 
 structure Type_Infer: TYPE_INFER =
@@ -99,14 +100,22 @@
 
 (* fixate -- introduce fresh type variables *)
 
-fun fixate ctxt ts =
+val object_logic =
+  Config.bool (Config.declare ("Type_Infer.object_logic", @{here}) (K (Config.Bool true)));
+
+fun fixate ctxt pattern ts =
   let
+    val base_sort = Object_Logic.get_base_sort ctxt;
+    val improve_sort =
+      if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
+      then fn [] => the base_sort | S => S else I;
+
     fun subst_param (xi, S) (inst, used) =
       if is_param xi then
         let
           val [a] = Name.invent used Name.aT 1;
           val used' = Name.declare a used;
-        in (((xi, S), TFree (a, S)) :: inst, used') end
+        in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
       else (inst, used);
     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
diff -r f59ef58f420b -r 8b85a554c5c4 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/variable.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -230,9 +230,6 @@
 
 (* constraints *)
 
-fun constrain_var (xi, T) =
-  if T = dummyT then Vartab.delete_safe xi else Vartab.update (xi, T);
-
 fun constrain_tvar (xi, raw_S) =
   let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
@@ -240,8 +237,8 @@
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let
     val types' = fold_aterms
-      (fn Free (x, T) => constrain_var ((x, ~1), T)
-        | Var v => constrain_var v
+      (fn Free (x, T) => Vartab.update ((x, ~1), T)
+        | Var v => Vartab.update v
         | _ => I) t types;
     val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
diff -r f59ef58f420b -r 8b85a554c5c4 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Tools/induct.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -172,7 +172,7 @@
 
 val rearrange_eqs_simproc =
   Simplifier.make_simproc @{context} "rearrange_eqs"
-   {lhss = [@{term "Pure.all(t)"}],
+   {lhss = [@{term "Pure.all (t :: 'a::{} \<Rightarrow> prop)"}],
     proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
 
 
diff -r f59ef58f420b -r 8b85a554c5c4 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Tools/nbe.ML	Tue Apr 12 15:01:06 2016 +0200
@@ -544,7 +544,10 @@
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     fun type_infer t' =
-      Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
+      Syntax.check_term
+        (ctxt
+          |> Config.put Type_Infer.object_logic false
+          |> Config.put Type_Infer_Context.const_sorts false)
         (Type.constraint (fastype_of t_original) t');
     fun check_tvars t' =
       if null (Term.add_tvars t' []) then t'