src/Tools/adhoc_overloading.ML
changeset 55954 a29aefc88c8d
parent 55237 1e341728bae9
child 55955 e8f1bf005661
     1.1 --- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 13:44:01 2014 +0100
     1.3 @@ -220,7 +220,8 @@
     1.4  
     1.5  fun adhoc_overloading_cmd add raw_args lthy =
     1.6    let
     1.7 -    fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
     1.8 +    fun const_name ctxt =
     1.9 +      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false} dummyT;
    1.10      fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
    1.11      val args =
    1.12        raw_args