# HG changeset patch
# User Christian Sternagel
# Date 1376044463 -32400
# Node ID 47db379a6cf9c3289dcfcfead05e75f42ec3c6ba
# Parent  38165b99562ea985431641aa5051604cc0ac5fc4
move treatment of polymorphism to adhoc overloading command;

diff -r 38165b99562e -r 47db379a6cf9 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Fri Aug 09 19:34:23 2013 +0900
+++ b/src/Tools/adhoc_overloading.ML	Fri Aug 09 19:34:23 2013 +0900
@@ -102,7 +102,7 @@
     let
       val ctxt = Context.proof_of context;
       val _ = if is_overloaded ctxt oconst then () else not_overloaded_error oconst;
-      val T = t |> singleton (Variable.polymorphic ctxt) |> fastype_of;
+      val T = t |> fastype_of;
       val t' = Term.map_types (K dummyT) t;
     in
       if add then
@@ -214,10 +214,11 @@
 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 read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args
       |> map (apfst (const_name lthy))
-      |> map (apsnd (map (Syntax.read_term lthy)));
+      |> map (apsnd (map (read_term lthy)));
   in
     Local_Theory.declaration {syntax = true, pervasive = false}
       (adhoc_overloading_cmd' add args) lthy