--- a/src/Tools/adhoc_overloading.ML Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Thu Mar 06 13:44:01 2014 +0100
@@ -220,7 +220,8 @@
fun adhoc_overloading_cmd add raw_args lthy =
let
- fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
+ fun const_name ctxt =
+ fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false} dummyT;
fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
val args =
raw_args