# HG changeset patch
# User haftmann
# Date 1284387312 -7200
# Node ID df86b1b4ce10d29fb459eab09ca664cdb26dcd76
# Parent  74469faa27cac685908f9e65475dc239e2e32e57
more precise name for activation of improveable syntax

diff -r 74469faa27ca -r df86b1b4ce10 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Sep 13 15:22:40 2010 +0200
+++ b/src/Pure/Isar/class.ML	Mon Sep 13 16:15:12 2010 +0200
@@ -293,7 +293,7 @@
   |> Variable.declare_term
       (Logic.mk_type (TFree (Name.aT, base_sort)))
   |> synchronize_class_syntax sort base_sort
-  |> Overloading.add_improvable_syntax;
+  |> Overloading.activate_improvable_syntax;
 
 fun init class thy =
   thy
@@ -548,7 +548,7 @@
     |> fold (Variable.declare_names o Free o snd) params
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
-    |> Overloading.add_improvable_syntax
+    |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
     |> Local_Theory.init NONE ""
diff -r 74469faa27ca -r df86b1b4ce10 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Sep 13 15:22:40 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Sep 13 16:15:12 2010 +0200
@@ -7,7 +7,7 @@
 signature OVERLOADING =
 sig
   type improvable_syntax
-  val add_improvable_syntax: Proof.context -> Proof.context
+  val activate_improvable_syntax: Proof.context -> Proof.context
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
@@ -104,7 +104,7 @@
     val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
   in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
 
-val add_improvable_syntax =
+val activate_improvable_syntax =
   Context.proof_map
     (Syntax.add_term_check 0 "improvement" improve_term_check
     #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
@@ -183,7 +183,7 @@
     |> ProofContext.init_global
     |> Data.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> add_improvable_syntax
+    |> activate_improvable_syntax
     |> synchronize_syntax
     |> Local_Theory.init NONE ""
        {define = Generic_Target.define foundation,