src/Pure/Isar/class.ML
changeset 39378 df86b1b4ce10
parent 39134 917b4b6ba3d2
child 39438 c5ece2a7a86e
     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 ""