# HG changeset patch
# User Christian Sternagel
# Date 1380546106 -32400
# Node ID e13b0c88c7986418dc288b471baa068d2859335d
# Parent  c4343c31f86d43582757cbeb19603a67098e433c
preserve types during rewriting

diff -r c4343c31f86d -r e13b0c88c798 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Mon Sep 30 22:36:43 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Mon Sep 30 22:01:46 2013 +0900
@@ -165,12 +165,15 @@
       | _ => oconst)
   | insert_variants _ _ oconst = oconst;
 
-fun insert_overloaded ctxt variant =
-  (case try Term.type_of variant of
-    NONE => variant
-  | SOME T =>
-    Pattern.rewrite_term (Proof_Context.theory_of ctxt) []
-      [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant);
+fun insert_overloaded ctxt =
+  let
+    fun proc t =
+      Term.map_types (K dummyT) t
+      |> get_overloaded ctxt
+      |> Option.map (Const o rpair (Term.type_of t));
+  in
+    Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc]
+  end;
 
 fun check ctxt =
   map (fn t => Term.map_aterms (insert_variants ctxt t) t);