diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -139,19 +139,18 @@
           (fn T as TFree _ => T | T as TVar (vi, _) =>
             if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
       end;
-    fun add_typ_check level name f = Context.proof_map
-      (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
-        let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
 
     (* preprocessing elements, retrieving base sort from type-checked elements *)
-    val raw_supexpr = (map (fn sup => (sup, (("", false),
-      Expression.Positional []))) sups, []);
-    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
+    val raw_supexpr =
+      (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
+    val init_class_body =
+      fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
-      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
-    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
-      |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
+      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
+      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
+    val ((raw_supparams, _, raw_inferred_elems), _) =
+      Proof_Context.init_global thy
+      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e
@@ -165,7 +164,7 @@
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
-          fold_types f t #> (fold o fold_types) f ts) o snd) assms
+          fold_types f t #> (fold o fold_types) f ts) o snd) assms;
     val base_sort = if null inferred_elems then proto_base_sort else
       case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
        of [] => error "No type variable in class specification"