more precise name for activation of improveable syntax
authorhaftmann
Mon Sep 13 16:15:12 2010 +0200 (2010-09-13 ago)
changeset 39378df86b1b4ce10
parent 39309 74469faa27ca
child 39379 ab1b070aa412
more precise name for activation of improveable syntax
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Sep 13 15:22:40 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Sep 13 16:15:12 2010 +0200
     1.3 @@ -293,7 +293,7 @@
     1.4    |> Variable.declare_term
     1.5        (Logic.mk_type (TFree (Name.aT, base_sort)))
     1.6    |> synchronize_class_syntax sort base_sort
     1.7 -  |> Overloading.add_improvable_syntax;
     1.8 +  |> Overloading.activate_improvable_syntax;
     1.9  
    1.10  fun init class thy =
    1.11    thy
    1.12 @@ -548,7 +548,7 @@
    1.13      |> fold (Variable.declare_names o Free o snd) params
    1.14      |> (Overloading.map_improvable_syntax o apfst)
    1.15           (K ((primary_constraints, []), (((improve, K NONE), false), [])))
    1.16 -    |> Overloading.add_improvable_syntax
    1.17 +    |> Overloading.activate_improvable_syntax
    1.18      |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
    1.19      |> synchronize_inst_syntax
    1.20      |> Local_Theory.init NONE ""
     2.1 --- a/src/Pure/Isar/overloading.ML	Mon Sep 13 15:22:40 2010 +0200
     2.2 +++ b/src/Pure/Isar/overloading.ML	Mon Sep 13 16:15:12 2010 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  signature OVERLOADING =
     2.5  sig
     2.6    type improvable_syntax
     2.7 -  val add_improvable_syntax: Proof.context -> Proof.context
     2.8 +  val activate_improvable_syntax: Proof.context -> Proof.context
     2.9    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
    2.10      -> Proof.context -> Proof.context
    2.11    val set_primary_constraints: Proof.context -> Proof.context
    2.12 @@ -104,7 +104,7 @@
    2.13      val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
    2.14    in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
    2.15  
    2.16 -val add_improvable_syntax =
    2.17 +val activate_improvable_syntax =
    2.18    Context.proof_map
    2.19      (Syntax.add_term_check 0 "improvement" improve_term_check
    2.20      #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
    2.21 @@ -183,7 +183,7 @@
    2.22      |> ProofContext.init_global
    2.23      |> Data.put overloading
    2.24      |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
    2.25 -    |> add_improvable_syntax
    2.26 +    |> activate_improvable_syntax
    2.27      |> synchronize_syntax
    2.28      |> Local_Theory.init NONE ""
    2.29         {define = Generic_Target.define foundation,