more rigid const demands, based on educated guesses about the tools involved here;

--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 16:24:47 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 16:33:48 2014 +0100
@@ -535,9 +535,9 @@
 
     val ctxt = Proof_Context.init_global thy9;
     val case_combs =
-      map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names;
+      map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
     val constrss = map (fn (dtname, {descr, index, ...}) =>
-      map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst)
+      map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
         (#3 (the (AList.lookup op = descr index)))) dt_infos;
   in
     thy9

--- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 16:24:47 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 16:33:48 2014 +0100
@@ -516,7 +516,7 @@
   Attrib.setup @{binding ind_realizer}
     ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
       Scan.option (Scan.lift (Args.colon) |--
-        Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
+        Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
     "add realizers for inductive set";
 
 end;

--- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 16:24:47 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 16:33:48 2014 +0100
@@ -221,7 +221,7 @@
 fun adhoc_overloading_cmd add raw_args lthy =
   let
     fun const_name ctxt =
-      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};
+      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};  (* FIXME {proper = true, strict = true} (!?) *)
     fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args