src/Pure/Isar/class_target.ML
changeset 32379 a97e9caebd60
parent 32074 76d6ba08a05f
child 32805 9b535493ac8d
     1.1 --- a/src/Pure/Isar/class_target.ML	Sat Aug 15 15:29:53 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sat Aug 15 15:29:54 2009 +0200
     1.3 @@ -513,6 +513,7 @@
     1.4        | NONE => NONE;
     1.5    in
     1.6      thy
     1.7 +    |> Theory.checkpoint
     1.8      |> ProofContext.init
     1.9      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.10      |> fold (Variable.declare_typ o TFree) vs