--- 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