# HG changeset patch
# User haftmann
# Date 1248960078 -7200
# Node ID 605877054de7343dc6b68a3863c97544c741bebf
# Parent  3fabf5b5fc838752eccc5cbc2f922e46b41d6969
improved handling of parameters

diff -r 3fabf5b5fc83 -r 605877054de7 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Jul 30 15:20:57 2009 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Jul 30 15:21:18 2009 +0200
@@ -132,36 +132,42 @@
   |> get_first (fn ((c, _), (v, checked)) =>
       if Binding.name_of b = v then SOME (c, checked) else NONE);
 
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
+
+(* target *)
 
+fun synchronize_syntax ctxt =
+  let
+    val overloading = OverloadingData.get ctxt;
+    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
+     of SOME (v, _) => SOME (ty, Free (v, ty))
+      | NONE => NONE;
+    val unchecks =
+      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
+  in 
+    ctxt
+    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+  end
 
-(* overloaded declarations and definitions *)
+fun init raw_overloading thy =
+  let
+    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
+  in
+    thy
+    |> ProofContext.init
+    |> OverloadingData.put overloading
+    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+    |> add_improvable_syntax
+    |> synchronize_syntax
+  end;
 
 fun declare c_ty = pair (Const c_ty);
 
 fun define checked b (c, t) = Thm.add_def (not checked) true
   (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
 
-
-(* target *)
-
-fun init raw_overloading thy =
-  let
-    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
-    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
-    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
-     of SOME (v, _) => SOME (ty, Free (v, ty))
-      | NONE => NONE;
-    val unchecks =
-      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
-  in
-    thy
-    |> ProofContext.init
-    |> OverloadingData.put overloading
-    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
-    |> add_improvable_syntax
-  end;
+fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
+  #> LocalTheory.target synchronize_syntax
 
 fun conclude lthy =
   let