src/Pure/Isar/class.ML

       (case lookup_inst_param (c, ty) of
         SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
       | NONE => NONE);
   in
     thy
-    |> Theory.checkpoint
     |> Proof_Context.init_global
     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) params
     |> (Overloading.map_improvable_syntax o apfst)